Physlib Documentation

Physlib.Mathematics.RatComplexNum

Rational complex numbers #

structure Physlib.RatComplexNum :

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.

Instances For

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

x = y

theorem Physlib.RatComplexNum.ext_iff {x y : RatComplexNum} :

x = y ↔ x.fst = y.fst ∧ x.snd = y.snd

def Physlib.RatComplexNum.equivToProd :

RatComplexNum ≃ ℚ × ℚ

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

Equations

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

Instances For

instance Physlib.RatComplexNum.instDecidableEq :

DecidableEq RatComplexNum

Equations

Physlib.RatComplexNum.instDecidableEq = Physlib.RatComplexNum.equivToProd.decidableEq

instance Physlib.RatComplexNum.instAdd :

Add RatComplexNum

Equations

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

@[simp]

theorem Physlib.RatComplexNum.add_fst (x y : RatComplexNum) :

(x + y).fst = x.fst + y.fst

@[simp]

theorem Physlib.RatComplexNum.add_snd (x y : RatComplexNum) :

(x + y).snd = x.snd + y.snd

instance Physlib.RatComplexNum.instAddCommGroup :

AddCommGroup RatComplexNum

Equations

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

instance Physlib.RatComplexNum.instMul :

Mul RatComplexNum

Equations

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

@[simp]

theorem Physlib.RatComplexNum.mul_fst (x y : RatComplexNum) :

(x * y).fst = x.fst * y.fst - x.snd * y.snd

@[simp]

theorem Physlib.RatComplexNum.mul_snd (x y : RatComplexNum) :

(x * y).snd = x.fst * y.snd + x.snd * y.fst

instance Physlib.RatComplexNum.instRing :

Ring RatComplexNum

Equations

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

@[simp]

theorem Physlib.RatComplexNum.one_fst :

fst 1 = 1

@[simp]

theorem Physlib.RatComplexNum.one_snd :

snd 1 = 0

@[simp]

theorem Physlib.RatComplexNum.zero_fst :

fst 0 = 0

@[simp]

theorem Physlib.RatComplexNum.zero_snd :

snd 0 = 0

noncomputable def Physlib.RatComplexNum.toComplexNum :

RatComplexNum →+* ℂ

The inclusion of RatComplexNum into the complex numbers.

Equations

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

Instances For

@[simp]

theorem Physlib.RatComplexNum.I_mul_toComplexNum (a : RatComplexNum) :

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

theorem Physlib.RatComplexNum.ofNat_mul_toComplexNum (n : ℕ) (a : RatComplexNum) :

↑n * toComplexNum a = toComplexNum (↑n * a)

theorem Physlib.RatComplexNum.toComplexNum_injective :

Function.Injective ⇑toComplexNum