Complex numbers

Content created by Louis Wasserman.

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

module complex-numbers where

open import complex-numbers.addition-complex-numbers public
open import complex-numbers.apartness-complex-numbers public
open import complex-numbers.complex-numbers public
open import complex-numbers.conjugation-complex-numbers public
open import complex-numbers.eisenstein-integers public
open import complex-numbers.gaussian-integers public
open import complex-numbers.large-additive-group-of-complex-numbers public
open import complex-numbers.large-ring-of-complex-numbers public
open import complex-numbers.magnitude-complex-numbers public
open import complex-numbers.multiplication-complex-numbers public
open import complex-numbers.multiplicative-inverses-nonzero-complex-numbers public
open import complex-numbers.nonzero-complex-numbers public
open import complex-numbers.raising-universe-levels-complex-numbers public
open import complex-numbers.similarity-complex-numbers public

Recent changes