Addition of complex numbers

Content created by Louis Wasserman.

Created on 2025-10-11.
Last modified on 2025-10-11.

module complex-numbers.addition-complex-numbers where
Imports 
open import complex-numbers.complex-numbers
open import complex-numbers.similarity-complex-numbers

open import foundation.action-on-identifications-binary-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import real-numbers.addition-real-numbers

Idea

We introduce addition on the complex numbers by componentwise addition of the real and imaginary parts.

Definition

add-ℂ : {l1 l2 : Level} → ℂ l1 → ℂ l2 → ℂ (l1 ⊔ l2)
add-ℂ (a , b) (c , d) = (a +ℝ c , b +ℝ d)

infixl 35 _+ℂ_
_+ℂ_ : {l1 l2 : Level} → ℂ l1 → ℂ l2 → ℂ (l1 ⊔ l2)
_+ℂ_ = add-ℂ

ap-add-ℂ :
  {l1 l2 : Level} →
  {x x' : ℂ l1} → x ＝ x' → {y y' : ℂ l2} → y ＝ y' →
  x +ℂ y ＝ x' +ℂ y'
ap-add-ℂ = ap-binary add-ℂ

Properties

Addition is commutative

abstract
  commutative-add-ℂ : {l1 l2 : Level} (x : ℂ l1) (y : ℂ l2) → x +ℂ y ＝ y +ℂ x
  commutative-add-ℂ _ _ = eq-ℂ (commutative-add-ℝ _ _) (commutative-add-ℝ _ _)

Addition is associative

abstract
  associative-add-ℂ :
    {l1 l2 l3 : Level} (x : ℂ l1) (y : ℂ l2) (z : ℂ l3) →
    (x +ℂ y) +ℂ z ＝ x +ℂ (y +ℂ z)
  associative-add-ℂ _ _ _ =
    eq-ℂ (associative-add-ℝ _ _ _) (associative-add-ℝ _ _ _)

Unit laws of addition

abstract
  left-unit-law-add-ℂ : {l : Level} (x : ℂ l) → zero-ℂ +ℂ x ＝ x
  left-unit-law-add-ℂ (a , b) =
    eq-ℂ (left-unit-law-add-ℝ a) (left-unit-law-add-ℝ b)

  right-unit-law-add-ℂ : {l : Level} (x : ℂ l) → x +ℂ zero-ℂ ＝ x
  right-unit-law-add-ℂ (a , b) =
    eq-ℂ (right-unit-law-add-ℝ a) (right-unit-law-add-ℝ b)

Inverse laws of addition

abstract
  left-inverse-law-add-ℂ : {l : Level} (x : ℂ l) → sim-ℂ (neg-ℂ x +ℂ x) zero-ℂ
  left-inverse-law-add-ℂ (a , b) =
    ( left-inverse-law-add-ℝ a , left-inverse-law-add-ℝ b)

  right-inverse-law-add-ℂ :
    {l : Level} (x : ℂ l) → sim-ℂ (x +ℂ neg-ℂ x) zero-ℂ
  right-inverse-law-add-ℂ (a , b) =
    ( right-inverse-law-add-ℝ a , right-inverse-law-add-ℝ b)

Recent changes