1.9. Inversion🔗

instance : Inv ℚ[i] := ⟨fun z => conj z * ((normSq z)⁻¹ : ℚ)⟩ theorem inv_def (z : ℚ[i]) : z⁻¹ = conj z * ((normSq z)⁻¹ : ℚ) := rfl @[simp] theorem inv_re (z : ℚ[i]) : z⁻¹.re = z.re / normSq z := byz:ℚ[i]⊢ z⁻¹.re = z.re / normSq z simp [inv_def, division_def]All goals completed! 🐙 @[simp] theorem inv_im (z : ℚ[i]) : z⁻¹.im = -z.im / normSq z := byz:ℚ[i]⊢ z⁻¹.im = -z.im / normSq z simp [inv_def, division_def]All goals completed! 🐙 @[simp, norm_cast] theorem ofRational_inv (r : ℚ) : ((r⁻¹ : ℚ) : ℚ[i]) = (r : ℚ[i])⁻¹ := byr:ℚ⊢ ↑r⁻¹ = (↑r)⁻¹ apply ext_iff.2r:ℚ⊢ (↑r⁻¹).re = (↑r)⁻¹.re ∧ (↑r⁻¹).im = (↑r)⁻¹.im simp [normSq]All goals completed! 🐙 protected theorem complexQ.inv_zero : (0⁻¹ : ℚ[i]) = 0 := by⊢ 0⁻¹ = 0 rw [← ofRational_zero]⊢ (↑0)⁻¹ = ↑0 rw [← ofRational_inv]⊢ ↑0⁻¹ = ↑0 rw [inv_zero]All goals completed! 🐙 protected theorem complexQ.mul_inv_cancel {z : ℚ[i]} (h : z ≠ 0) : z * z⁻¹ = 1 := byz:ℚ[i]h:z ≠ 0⊢ z * z⁻¹ = 1 rw [inv_def]z:ℚ[i]h:z ≠ 0⊢ z * ((starRingEnd ℚ[i]) z * ↑(normSq z)⁻¹) = 1 rw [← mul_assoc]z:ℚ[i]h:z ≠ 0⊢ z * (starRingEnd ℚ[i]) z * ↑(normSq z)⁻¹ = 1 rw [mul_conj]z:ℚ[i]h:z ≠ 0⊢ ↑(normSq z) * ↑(normSq z)⁻¹ = 1 rw [← ofRational_mul]z:ℚ[i]h:z ≠ 0⊢ ↑(normSq z * (normSq z)⁻¹) = 1 norm_castz:ℚ[i]h:z ≠ 0⊢ normSq z * (normSq z)⁻¹ = 1 exact mul_inv_cancel₀ (mt normSq_eq_zero.1 h)All goals completed! 🐙 -- an instance of monoid with inverse and division -- After ths point we can use the division operator instance instDivInvMonoid : DivInvMonoid ℚ[i] where (3 : Rat)/2 + (1 : Rat)/2*I#eval (2-I)/(1-I) -- relation between division and -- the real part and imaginary part lemma div_re (z w : ℚ[i]) : (z / w).re = z.re * w.re / normSq w + z.im * w.im / normSq w := byz:ℚ[i]w:ℚ[i]⊢ (z / w).re = z.re * w.re / normSq w + z.im * w.im / normSq w simp [div_eq_mul_inv, mul_assoc, sub_eq_add_neg]All goals completed! 🐙 lemma div_im (z w : ℚ[i]) : (z / w).im = z.im * w.re / normSq w - z.re * w.im / normSq w := byz:ℚ[i]w:ℚ[i]⊢ (z / w).im = z.im * w.re / normSq w - z.re * w.im / normSq w simp [div_eq_mul_inv,mul_assoc,sub_eq_add_neg,add_comm]All goals completed! 🐙