Addition of nonzero complex numbers

Content created by Louis Wasserman.

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

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

open import foundation.disjunction
open import foundation.functoriality-disjunction
open import foundation.universe-levels

open import real-numbers.addition-nonzero-real-numbers
open import real-numbers.nonzero-real-numbers

Idea

This file describes properties of addition of nonzero complex numbers.

Properties

If the sum of two complex numbers is nonzero, one of them is nonzero

abstract
  is-nonzero-either-is-nonzero-add-ℂ :
    {l1 l2 : Level} (z : ℂ l1) (w : ℂ l2) → is-nonzero-ℂ (z +ℂ w) →
    disjunction-type (is-nonzero-ℂ z) (is-nonzero-ℂ w)
  is-nonzero-either-is-nonzero-add-ℂ z@(a +iℂ b) w@(c +iℂ d) =
    elim-disjunction
      ( is-nonzero-prop-ℂ z ∨ is-nonzero-prop-ℂ w)
      ( λ a+c≠0 →
        map-disjunction
          ( inl-disjunction)
          ( inl-disjunction)
          ( is-nonzero-either-is-nonzero-add-ℝ a c a+c≠0))
      ( λ b+d≠0 →
        map-disjunction
          ( inr-disjunction)
          ( inr-disjunction)
          ( is-nonzero-either-is-nonzero-add-ℝ b d b+d≠0))

Recent changes