Conjugation of complex numbers

Content created by Louis Wasserman.

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

module complex-numbers.conjugation-complex-numbers where
Imports 
open import complex-numbers.complex-numbers

open import foundation.identity-types
open import foundation.universe-levels

open import real-numbers.negation-real-numbers

Idea

The conjugate of a complex number a + bi is a - bi.

Definition

conjugate-ℂ : {l : Level} → ℂ l → ℂ l
conjugate-ℂ (a +iℂ b) = a +iℂ neg-ℝ b

Properties

Conjugation is an involution

abstract
  is-involution-conjugate-ℂ :
    {l : Level} (z : ℂ l) → conjugate-ℂ (conjugate-ℂ z) ＝ z
  is-involution-conjugate-ℂ (a +iℂ b) = eq-ℂ refl (neg-neg-ℝ b)

Recent changes