Metamath Proof Explorer


Table of Contents - 21.20.6.8. Argument, multiplication and inverse

Since one needs arguments in order to define multiplication in , and one needs complex multiplication in order to define arguments, it would be contrived to construct a whole theory for a temporary multiplication (and temporary powers, then temporary logarithm, and finally temporary argument) before redefining the extended complex multiplication. Therefore, we adopt a two-step process, see df-bj-mulc.

  1. carg
  2. df-bj-arg
  3. cmulc
  4. df-bj-mulc
  5. cinvc
  6. df-bj-invc