Metamath Proof Explorer


Table of Contents - 21.20.6.6. Addition and opposite

We define the operations of addition and opposite on the extended complex numbers and on the complex projective line (Riemann sphere) simultaneously, thus "overloading" the operations.

  1. caddcc
  2. df-bj-addc
  3. coppcc
  4. df-bj-oppc