Rational complex numbers

structure PhysLean.RatComplexNum : Type

Rational complex numbers. This type is mainly used when decidability is needed.

• fst : ℚ

  The real part of a RatComplexNum.

• snd : ℚ

  The imaginary part of a RatComplexNum.

theorem PhysLean.RatComplexNum.ext {x y : RatComplexNum} (h1 : x.fst = y.fst) (h2 : x.snd = y.snd) : x = y

theorem PhysLean.RatComplexNum.ext_iff {x y : RatComplexNum} : x = y ↔ x.fst = y.fst ∧ x.snd = y.snd

def PhysLean.RatComplexNum.equivToProd : RatComplexNum ≃ ℚ × ℚ

The equivalence as a type of RatComplexNum with ℚ × ℚ.

Equations

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

instance PhysLean.RatComplexNum.instDecidableEq : DecidableEq RatComplexNum

Equations

• PhysLean.RatComplexNum.instDecidableEq = PhysLean.RatComplexNum.equivToProd.decidableEq

instance PhysLean.RatComplexNum.instAdd : Add RatComplexNum

Equations

• PhysLean.RatComplexNum.instAdd = { add := fun (x y : PhysLean.RatComplexNum) => { fst := x.fst + y.fst, snd := x.snd + y.snd } }

@[simp]

theorem PhysLean.RatComplexNum.add_fst (x y : RatComplexNum) : (x + y).fst = x.fst + y.fst

@[simp]

theorem PhysLean.RatComplexNum.add_snd (x y : RatComplexNum) : (x + y).snd = x.snd + y.snd

instance PhysLean.RatComplexNum.instAddCommGroup : AddCommGroup RatComplexNum

Equations

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

instance PhysLean.RatComplexNum.instMul : Mul RatComplexNum

Equations

• PhysLean.RatComplexNum.instMul = { mul := fun (x y : PhysLean.RatComplexNum) => { fst := x.fst * y.fst - x.snd * y.snd, snd := x.fst * y.snd + x.snd * y.fst } }

@[simp]

theorem PhysLean.RatComplexNum.mul_fst (x y : RatComplexNum) : (x * y).fst = x.fst * y.fst - x.snd * y.snd

@[simp]

theorem PhysLean.RatComplexNum.mul_snd (x y : RatComplexNum) : (x * y).snd = x.fst * y.snd + x.snd * y.fst

instance PhysLean.RatComplexNum.instRing : Ring RatComplexNum

Equations

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

@[simp]

theorem PhysLean.RatComplexNum.one_fst : fst 1 = 1

@[simp]

theorem PhysLean.RatComplexNum.one_snd : snd 1 = 0

@[simp]

theorem PhysLean.RatComplexNum.zero_fst : fst 0 = 0

@[simp]

theorem PhysLean.RatComplexNum.zero_snd : snd 0 = 0

noncomputable def PhysLean.RatComplexNum.toComplexNum : RatComplexNum →+* ℂ

The inclusion of RatComplexNum into the complex numbers.

Equations

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

@[simp]

theorem PhysLean.RatComplexNum.I_mul_toComplexNum (a : RatComplexNum) : Complex.I * toComplexNum a = toComplexNum ({ fst := 0, snd := 1 } * a)

theorem PhysLean.RatComplexNum.ofNat_mul_toComplexNum (n : ℕ) (a : RatComplexNum) : ↑n * toComplexNum a = toComplexNum (↑n * a)

theorem PhysLean.RatComplexNum.toComplexNum_injective : Function.Injective ⇑toComplexNum