For a few other examples, you can look at the subsection "21.29.8.2 Complex numbers (supplements)" (beginning with ~bj-subcom), in my mathbox. They are in deduction form and for most of them, the conclusion is an equivalence. There are a few other algebraic lemmas in other mathboxes as well. In my case, I haven't tried to be systematic and haven't thought too much about the most economical way to treat these, but I used some of them to prove a formula for barycentric coordinates in ~bj-bary1.
Benoit -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/36b5950e-055b-46d8-a04a-8621dcee127f%40googlegroups.com.
