1.2. Arithemtic operations🔗

instance : Add ℚ[i] := ⟨fun x y => ⟨ x.re + y.re, x.im + y.im⟩ ⟩ instance : Mul ℚ[i] := ⟨fun x y => ⟨ x.re*y.re - x.im*y.im, x.re*y.im + x.im*y.re⟩ ⟩ instance : Neg ℚ[i] := ⟨fun x => ⟨-x.re, -x.im⟩⟩ 0 + 3*I#eval -sample2 -- Subtraction will be defined in terms of addition -- and negative. 0 + -2*I#eval sample2 + I -- 0 + -2*I 3 + 0*I#eval sample3*I -- 3 + 0*I -- Some properties that are true by definition @[simp] lemma zero_re : (0:ℚ[i]).re = 0 := rfl @[simp] lemma zero_im : (0:ℚ[i]).im = 0 := rfl @[simp] lemma one_re : (1:ℚ[i]).re = 1 := rfl @[simp] lemma one_im : (1:ℚ[i]).im = 0 := rfl @[simp] lemma add_re (x y : ℚ[i]) : (x+y).re = x.re+y.re := rfl @[simp] lemma add_im (x y : ℚ[i]) : (x+y).im = x.im+y.im := rfl @[simp] lemma neg_re (x : ℚ[i]) : (-x).re = -x.re := rfl @[simp] lemma neg_im (x : ℚ[i]) : (-x).im = -x.im := rfl @[simp] lemma mul_re (x y: ℚ[i]) : (x*y).re = x.re*y.re - x.im*y.im := rfl @[simp] lemma mul_im (x y: ℚ[i]) : (x*y).im = x.re*y.im + x.im*y.re := rfl @[simp] lemma zero_def : (0 : ℚ[i]) = ⟨0,0⟩ := rfl @[simp] lemma one_def : (1 : ℚ[i]) = ⟨1,0⟩ := rfl @[simp] lemma I_re : I.re = 0 := rfl @[simp] lemma I_im : I.im = 1 := rfl @[simp] lemma I_mul_I : I*I = -1 := ext_iff.mpr <| by⊢ (I * I).re = (-1).re ∧ (I * I).im = (-1).im simpAll goals completed! 🐙 theorem I_mul (z:ℚ[i]) : I*z = ⟨ -z.im, z.re⟩ := ext_iff.mpr <| byz:ℚ[i]⊢ (I * z).re = { re := -z.im, im := z.re }.re ∧ (I * z).im = { re := -z.im, im := z.re }.im simpAll goals completed! 🐙 -- mt stands for modus tollens @[simp] lemma I_ne_zero : (I:ℚ[i]) ≠ 0 := mt (congr_arg (fun z:ℚ[i] => z.im)) zero_ne_one.symm @[simp] theorem eta : ∀ z : complexQ, complexQ.mk z.re z.im = z := by⊢ ∀ (z : ℚ[i]), { re := z.re, im := z.im } = z intro zz:ℚ[i]⊢ { re := z.re, im := z.im } = z cases' z with x ymkx:ℚy:ℚ⊢ { re := { re := x, im := y }.re, im := { re := x, im := y }.im } = { re := x, im := y } dsimpAll goals completed! 🐙 -- `ℚ[i]` is equivalent to `ℚ × ℚ` @[simps apply] def equivRationalProd : ℚ[i] ≃ ℚ×ℚ where toFun z := ⟨z.re, z.im⟩ invFun p := ⟨p.1, p.2⟩ left_inv := fun ⟨ _, _ ⟩ => rfl right_inv := fun ⟨ _, _ ⟩ => rfl theorem ext : ∀ {z w : ℚ[i]}, z.re = w.re → z.im = w.im → z = w | ⟨_, _⟩, ⟨_, _⟩, rfl, rfl => rfl attribute [local ext] complexQ.ext