For a few other examples, you can look at the subsection "  
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.


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 view this discussion on the web visit

Reply via email to