structure Data.Complex (α : Type u) : Type u

A complex number $z = \text{re} + \text{im} \cdot i$ over a type α.

$$\mathbb{C}(\alpha) = \{ a + bi \mid a, b \in \alpha \}$$

Provides addition, multiplication, conjugation, and magnitude squared.

• re : α

  The real part: $\text{Re}(z)$.

• im : α

  The imaginary part: $\text{Im}(z)$.

@[implicit_reducible]

instance Data.instBEqComplex {α✝ : Type u_1} [BEq α✝] : BEq (Complex α✝)

Equations

• Data.instBEqComplex = { beq := Data.instBEqComplex.beq }

def Data.instBEqComplex.beq {α✝ : Type u_1} [BEq α✝] : Complex α✝ → Complex α✝ → Bool

Equations

• Data.instBEqComplex.beq { re := a, im := a_1 } { re := b, im := b_1 } = (a == b && a_1 == b_1)
• Data.instBEqComplex.beq x✝¹ x✝ = false

def Data.instOrdComplex.ord {α✝ : Type u_1} [Ord α✝] : Complex α✝ → Complex α✝ → Ordering

Equations

• Data.instOrdComplex.ord { re := a, im := a_1 } { re := b, im := b_1 } = (compare a b).then ((compare a_1 b_1).then Ordering.eq)

@[implicit_reducible]

instance Data.instOrdComplex {α✝ : Type u_1} [Ord α✝] : Ord (Complex α✝)

Equations

• Data.instOrdComplex = { compare := Data.instOrdComplex.ord }

@[implicit_reducible]

instance Data.instReprComplex {α✝ : Type u_1} [Repr α✝] : Repr (Complex α✝)

Equations

• Data.instReprComplex = { reprPrec := Data.instReprComplex.repr }

def Data.instReprComplex.repr {α✝ : Type u_1} [Repr α✝] : Complex α✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.instHashableComplex {α✝ : Type u_1} [Hashable α✝] : Hashable (Complex α✝)

Equations

• Data.instHashableComplex = { hash := Data.instHashableComplex.hash }

def Data.instHashableComplex.hash {α✝ : Type u_1} [Hashable α✝] : Complex α✝ → UInt64

Equations

• Data.instHashableComplex.hash { re := a, im := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[implicit_reducible]

instance Data.Complex.instInhabited {α : Type u_1} [Inhabited α] : Inhabited (Complex α)

Equations

• Data.Complex.instInhabited = { default := { re := default, im := default } }

@[implicit_reducible]

instance Data.Complex.instToString {α : Type u_1} [ToString α] : ToString (Complex α)

Equations

• Data.Complex.instToString = { toString := fun (z : Data.Complex α) => toString z.re ++ toString " + " ++ toString z.im ++ toString "i" }

@[inline]

def Data.Complex.ofReal {α : Type u_1} [OfNat α 0] (a : α) : Complex α

Construct a purely real complex number: $a + 0i$.

Equations

• Data.Complex.ofReal a = { re := a, im := 0 }

@[inline]

def Data.Complex.i {α : Type u_1} [OfNat α 0] [OfNat α 1] : Complex α

The imaginary unit: $i = 0 + 1i$.

Equations

• Data.Complex.i = { re := 0, im := 1 }

@[implicit_reducible]

instance Data.Complex.instAdd {α : Type u_1} [Add α] : Add (Complex α)

Addition of complex numbers: $$(a + bi) + (c + di) = (a + c) + (b + d)i$$

Equations

• Data.Complex.instAdd = { add := fun (z w : Data.Complex α) => { re := z.re + w.re, im := z.im + w.im } }

@[implicit_reducible]

instance Data.Complex.instNeg {α : Type u_1} [Neg α] : Neg (Complex α)

Negation: $-(a + bi) = -a + (-b)i$.

Equations

• Data.Complex.instNeg = { neg := fun (z : Data.Complex α) => { re := -z.re, im := -z.im } }

@[implicit_reducible]

instance Data.Complex.instSub {α : Type u_1} [Sub α] : Sub (Complex α)

Subtraction: $(a + bi) - (c + di) = (a - c) + (b - d)i$.

Equations

• Data.Complex.instSub = { sub := fun (z w : Data.Complex α) => { re := z.re - w.re, im := z.im - w.im } }

@[implicit_reducible]

instance Data.Complex.instMulOfAddOfSub {α : Type u_1} [Add α] [Sub α] [Mul α] : Mul (Complex α)

Multiplication of complex numbers: $$(a + bi)(c + di) = (ac - bd) + (ad + bc)i$$

Equations

• Data.Complex.instMulOfAddOfSub = { mul := fun (z w : Data.Complex α) => { re := z.re * w.re - z.im * w.im, im := z.re * w.im + z.im * w.re } }

def Data.Complex.conjugate {α : Type u_1} [Neg α] (z : Complex α) : Complex α

Complex conjugate: $\overline{a + bi} = a - bi$.

Satisfies $z \cdot \overline{z} = |z|^2$.

Equations

• z.conjugate = { re := z.re, im := -z.im }

def Data.Complex.magnitudeSquared {α : Type u_1} [Add α] [Mul α] (z : Complex α) : α

Magnitude squared (norm squared): $$|z|^2 = \text{Re}(z)^2 + \text{Im}(z)^2 = z \cdot \overline{z}$$

Returns a real value. Avoids square roots for exact arithmetic.

Equations

• z.magnitudeSquared = z.re * z.re + z.im * z.im

theorem Data.Complex.conjugate_conjugate {α : Type u_1} [Neg α] (hnn : ∀ (x : α), - -x = x) (z : Complex α) : z.conjugate.conjugate = z

Conjugation is an involution: $\overline{\overline{z}} = z$. $$\overline{\overline{a + bi}} = \overline{a - bi} = a + bi$$

Requires that negation is involutive: $-(-x) = x$.

theorem Data.Complex.add_comm' {α : Type u_1} [Add α] (hc : ∀ (a b : α), a + b = b + a) (z w : Complex α) : z + w = w + z

Addition is commutative: $(z_1 + z_2) = (z_2 + z_1)$.

Requires that the underlying type has commutative addition.