PhysLean Documentation

PhysLean.Mathematics.RatComplexNum

Rational complex numbers #

source
structure PhysLean.RatComplexNum :
Type

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

Instances For
    source
    theorem PhysLean.RatComplexNum.ext {x y : RatComplexNum} (h1 : x.fst = y.fst) (h2 : x.snd = y.snd) :
    x = y
    source
    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.
    Instances For
      source
      instance PhysLean.RatComplexNum.instDecidableEq :
      DecidableEq RatComplexNum
      Equations
      source
      instance PhysLean.RatComplexNum.instAddCommGroup :
      AddCommGroup RatComplexNum
      Equations
      source
      instance PhysLean.RatComplexNum.instRing :
      Ring RatComplexNum
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem PhysLean.RatComplexNum.one_fst :
      fst 1 = 1
      source
      @[simp]
      theorem PhysLean.RatComplexNum.one_snd :
      snd 1 = 0
      source
      @[simp]
      theorem PhysLean.RatComplexNum.add_fst (x y : RatComplexNum) :
      (x + y).fst = x.fst + y.fst
      source
      @[simp]
      theorem PhysLean.RatComplexNum.add_snd (x y : RatComplexNum) :
      (x + y).snd = x.snd + y.snd
      source
      @[simp]
      theorem PhysLean.RatComplexNum.mul_fst (x y : RatComplexNum) :
      (x * y).fst = x.fst * y.fst - x.snd * y.snd
      source
      @[simp]
      theorem PhysLean.RatComplexNum.mul_snd (x y : RatComplexNum) :
      (x * y).snd = x.fst * y.snd + x.snd * y.fst
      source
      @[simp]
      theorem PhysLean.RatComplexNum.zero_fst :
      fst 0 = 0
      source
      @[simp]
      theorem PhysLean.RatComplexNum.zero_snd :
      snd 0 = 0
      source
      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.
      Instances For
        source
        @[simp]
        theorem PhysLean.RatComplexNum.I_mul_toComplexNum (a : RatComplexNum) :
        Complex.I * toComplexNum a = toComplexNum ({ fst := 0, snd := 1 } * a)
        source
        theorem PhysLean.RatComplexNum.ofNat_mul_toComplexNum (n : ℕ) (a : RatComplexNum) :
        ↑n * toComplexNum a = toComplexNum (↑n * a)
        source
        theorem PhysLean.RatComplexNum.toComplexNum_injective :
        Function.Injective ⇑toComplexNum