1.5. Additive group structure
Here we show that ℚ[i] as an additive group.
instance addCommGroup : AddCommGroup ℚ[i] where
zero := (0:ℚ[i])
add := Add.add
-- sub := Sub.sub
neg := Neg.neg
nsmul := fun n z => n • z
zsmul := fun n z => n • z
add_assoc := ⊢ ∀ (a b c : ℚ[i]), a + b + c = a + (b + c)
a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝) ; a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝ + b✝ + c✝).re = (a✝ + (b✝ + c✝)).rea✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝ + b✝ + c✝).im = (a✝ + (b✝ + c✝)).im a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝ + b✝ + c✝).re = (a✝ + (b✝ + c✝)).rea✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝ + b✝ + c✝).im = (a✝ + (b✝ + c✝)).im All goals completed! 🐙
zero_add := ⊢ ∀ (a : ℚ[i]), 0 + a = a
a:ℚ[i]⊢ 0 + a = a; a:ℚ[i]⊢ (0 + a).re = a.rea:ℚ[i]⊢ (0 + a).im = a.im
a:ℚ[i]⊢ (0 + a).re = a.re a:ℚ[i]⊢ 0 + a.re = a.re
All goals completed! 🐙
a:ℚ[i]⊢ (0 + a).im = a.im a:ℚ[i]⊢ 0 + a.im = a.im
All goals completed! 🐙
add_zero := ⊢ ∀ (a : ℚ[i]), a + 0 = a
a:ℚ[i]⊢ a + 0 = a; a:ℚ[i]⊢ (a + 0).re = a.rea:ℚ[i]⊢ (a + 0).im = a.im
a:ℚ[i]⊢ (a + 0).re = a.re a:ℚ[i]⊢ a.re + 0 = a.re
All goals completed! 🐙
a:ℚ[i]⊢ (a + 0).im = a.im a:ℚ[i]⊢ a.im + 0 = a.im
All goals completed! 🐙
add_comm := ⊢ ∀ (a b : ℚ[i]), a + b = b + a
a:ℚ[i]b:ℚ[i]⊢ a + b = b + a
a:ℚ[i]b:ℚ[i]⊢ (a + b).re = (b + a).rea:ℚ[i]b:ℚ[i]⊢ (a + b).im = (b + a).im
a:ℚ[i]b:ℚ[i]⊢ (a + b).re = (b + a).re a:ℚ[i]b:ℚ[i]⊢ a.re + b.re = b.re + a.re
All goals completed! 🐙
a:ℚ[i]b:ℚ[i]⊢ (a + b).im = (b + a).im a:ℚ[i]b:ℚ[i]⊢ a.im + b.im = b.im + a.im
All goals completed! 🐙
neg_add_cancel := ⊢ ∀ (a : ℚ[i]), -a + a = 0
a:ℚ[i]⊢ -a + a = 0
a:ℚ[i]⊢ (-a + a).re = complexQ.re 0a:ℚ[i]⊢ (-a + a).im = complexQ.im 0
a:ℚ[i]⊢ (-a + a).re = complexQ.re 0 a:ℚ[i]⊢ -a.re + a.re = { re := 0, im := 0 }.re
All goals completed! 🐙
a:ℚ[i]⊢ (-a + a).im = complexQ.im 0 a:ℚ[i]⊢ -a.im + a.im = { re := 0, im := 0 }.im
All goals completed! 🐙
zsmul_zero' := ⊢ ∀ (a : ℚ[i]), 0 • a = 0
a✝:ℚ[i]⊢ 0 • a✝ = 0 ; a✝:ℚ[i]⊢ (0 • a✝).re = complexQ.re 0a✝:ℚ[i]⊢ (0 • a✝).im = complexQ.im 0 a✝:ℚ[i]⊢ (0 • a✝).re = complexQ.re 0a✝:ℚ[i]⊢ (0 • a✝).im = complexQ.im 0 a✝:ℚ[i]⊢ (0 • a✝).im = 0 a✝:ℚ[i]⊢ (0 • a✝).re = 0a✝:ℚ[i]⊢ (0 • a✝).im = 0 All goals completed! 🐙
nsmul_zero := ⊢ ∀ (x : ℚ[i]), 0 • x = 0
x✝:ℚ[i]⊢ 0 • x✝ = 0 ; x✝:ℚ[i]⊢ (0 • x✝).re = complexQ.re 0x✝:ℚ[i]⊢ (0 • x✝).im = complexQ.im 0 x✝:ℚ[i]⊢ (0 • x✝).re = complexQ.re 0x✝:ℚ[i]⊢ (0 • x✝).im = complexQ.im 0 x✝:ℚ[i]⊢ (0 • x✝).im = 0 x✝:ℚ[i]⊢ (0 • x✝).re = 0x✝:ℚ[i]⊢ (0 • x✝).im = 0 All goals completed! 🐙
nsmul_succ := ⊢ ∀ (n : ℕ) (x : ℚ[i]), (n + 1) • x = n • x + x
n✝:ℕx✝:ℚ[i]⊢ (n✝ + 1) • x✝ = n✝ • x✝ + x✝; n✝:ℕx✝:ℚ[i]⊢ ((n✝ + 1) • x✝).re = (n✝ • x✝ + x✝).ren✝:ℕx✝:ℚ[i]⊢ ((n✝ + 1) • x✝).im = (n✝ • x✝ + x✝).im n✝:ℕx✝:ℚ[i]⊢ ((n✝ + 1) • x✝).re = (n✝ • x✝ + x✝).ren✝:ℕx✝:ℚ[i]⊢ ((n✝ + 1) • x✝).im = (n✝ • x✝ + x✝).im All goals completed! 🐙
zsmul_succ' := ⊢ ∀ (n : ℕ) (a : ℚ[i]), ↑n.succ • a = ↑n • a + a
n✝:ℕa✝:ℚ[i]⊢ ↑n✝.succ • a✝ = ↑n✝ • a✝ + a✝; n✝:ℕa✝:ℚ[i]⊢ (↑n✝.succ • a✝).re = (↑n✝ • a✝ + a✝).ren✝:ℕa✝:ℚ[i]⊢ (↑n✝.succ • a✝).im = (↑n✝ • a✝ + a✝).im n✝:ℕa✝:ℚ[i]⊢ (↑n✝.succ • a✝).re = (↑n✝ • a✝ + a✝).ren✝:ℕa✝:ℚ[i]⊢ (↑n✝.succ • a✝).im = (↑n✝ • a✝ + a✝).im All goals completed! 🐙
zsmul_neg' := ⊢ ∀ (n : ℕ) (a : ℚ[i]), Int.negSucc n • a = -(↑n.succ • a)
n✝:ℕa✝:ℚ[i]⊢ Int.negSucc n✝ • a✝ = -(↑n✝.succ • a✝); n✝:ℕa✝:ℚ[i]⊢ (Int.negSucc n✝ • a✝).re = (-(↑n✝.succ • a✝)).ren✝:ℕa✝:ℚ[i]⊢ (Int.negSucc n✝ • a✝).im = (-(↑n✝.succ • a✝)).im n✝:ℕa✝:ℚ[i]⊢ (Int.negSucc n✝ • a✝).re = (-(↑n✝.succ • a✝)).ren✝:ℕa✝:ℚ[i]⊢ (Int.negSucc n✝ • a✝).im = (-(↑n✝.succ • a✝)).im All goals completed! 🐙
-- After verifying that the additive group structure,
-- we can now do subtraction
#eval sample1 - sample3
instance : One complexQ where
one := ⟨1, 0⟩
-- Casting from `ℕ` and `ℤ` to `ℚ[i]`
instance addGroupWithOne : AddGroupWithOne complexQ where
-- Inherit AddGroup from previously defined AddCommGroup
toAddGroup := inferInstance
-- Explicitly construct the '1' element
one := ⟨1, 0⟩
-- Explicitly state the typecast to ℚ
natCast n := ⟨(n : ℚ), 0⟩
natCast_zero := ⊢ { re := ↑0, im := 0 } = 0
⊢ { re := ↑0, im := 0 }.re = complexQ.re 0⊢ { re := ↑0, im := 0 }.im = complexQ.im 0
⊢ { re := ↑0, im := 0 }.re = complexQ.re 0 All goals completed! 🐙
⊢ { re := ↑0, im := 0 }.im = complexQ.im 0 All goals completed! 🐙
natCast_succ n := n:ℕ⊢ { re := ↑(n + 1), im := 0 } = { re := ↑n, im := 0 } + 1
n:ℕ⊢ { re := ↑n + 1, im := 0 } = { re := ↑n, im := 0 } + 1
n:ℕ⊢ { re := ↑n + 1, im := 0 }.re = ({ re := ↑n, im := 0 } + 1).ren:ℕ⊢ { re := ↑n + 1, im := 0 }.im = ({ re := ↑n, im := 0 } + 1).im
n:ℕ⊢ { re := ↑n + 1, im := 0 }.re = ({ re := ↑n, im := 0 } + 1).re -- Solves the real part: ↑(n + 1) = ↑n + 1
All goals completed! 🐙
n:ℕ⊢ { re := ↑n + 1, im := 0 }.im = ({ re := ↑n, im := 0 } + 1).im -- Solves the imaginary part: 0 = complexQ.im 1
n:ℕ⊢ 0 = ({ re := ↑n, im := 0 } + 1).im
All goals completed! 🐙
intCast n := ⟨(n : ℚ), 0⟩
intCast_ofNat n := n:ℕ⊢ { re := ↑↑n, im := 0 } = ↑n
n:ℕ⊢ { re := ↑↑n, im := 0 }.re = (↑n).ren:ℕ⊢ { re := ↑↑n, im := 0 }.im = (↑n).im
n:ℕ⊢ { re := ↑↑n, im := 0 }.re = (↑n).re n:ℕ⊢ ↑n = (↑n).re; All goals completed! 🐙
n:ℕ⊢ { re := ↑↑n, im := 0 }.im = (↑n).im All goals completed! 🐙
intCast_negSucc n := n:ℕ⊢ { re := ↑(Int.negSucc n), im := 0 } = -↑(n + 1)
n:ℕ⊢ { re := ↑(Int.negSucc n), im := 0 }.re = (-↑(n + 1)).ren:ℕ⊢ { re := ↑(Int.negSucc n), im := 0 }.im = (-↑(n + 1)).im
n:ℕ⊢ { re := ↑(Int.negSucc n), im := 0 }.re = (-↑(n + 1)).re n:ℕ⊢ -(↑n + 1) = (-↑(n + 1)).re
All goals completed! 🐙
n:ℕ⊢ { re := ↑(Int.negSucc n), im := 0 }.im = (-↑(n + 1)).im All goals completed! 🐙
-- Multiplication by integers are now enabled
#eval 4 * sample1
#eval (-2) * sample2