1.11. Field
Given all the previous preparation, we can now register ℚ[i] as
an instande of Field.
instance instField : Field ℚ[i] where
mul_inv_cancel := fun z hz =>
complexQ.mul_inv_cancel hz
inv_zero := complexQ.inv_zero
nnqsmul := (· • ·)
qsmul := (· • ·)
qsmul_def q z := ext_iff.2 <| q:ℚz:ℚ[i]⊢ (q • z).re = (↑q * z).re ∧ (q • z).im = (↑q * z).im All goals completed! 🐙
ratCast_def q := q:ℚ⊢ ↑q = ↑q.num / ↑q.den
q:ℚ⊢ (↑q).re = (↑q.num / ↑q.den).req:ℚ⊢ (↑q).im = (↑q.num / ↑q.den).im
q:ℚ⊢ (↑q).re = (↑q.num / ↑q.den).re q:ℚ⊢ q = (↑q.num / ↑q.den).re
q:ℚ⊢ q = ↑q.num * ↑q.den / (↑q.den * ↑q.den)
q:ℚ⊢ q = ↑q.num / ↑q.den
All goals completed! 🐙
q:ℚ⊢ (↑q).im = (↑q.num / ↑q.den).im q:ℚ⊢ 0 = (↑q.num / ↑q.den).im
All goals completed! 🐙
nnqsmul_def n z :=
ext_iff.2 <| n:ℚ≥0z:ℚ[i]⊢ (n • z).re = (↑n * z).re ∧ (n • z).im = (↑n * z).im All goals completed! 🐙
nnratCast_def q := q:ℚ≥0⊢ ↑q = ↑q.num / ↑q.den
q:ℚ≥0⊢ (↑q).re = (↑q.num / ↑q.den).req:ℚ≥0⊢ (↑q).im = (↑q.num / ↑q.den).im q:ℚ≥0⊢ (↑q).re = (↑q.num / ↑q.den).req:ℚ≥0⊢ (↑q).im = (↑q.num / ↑q.den).im
All goals completed! 🐙
@[simp, norm_cast]
lemma ofReal_nnqsmul (q : ℚ≥0) (r : ℚ)
: ofRational (q • r) = q • r := q:ℚ≥0r:ℚ⊢ ↑(q • r) = q • ↑r
q:ℚ≥0r:ℚ⊢ (↑(q • r)).re = (q • ↑r).req:ℚ≥0r:ℚ⊢ (↑(q • r)).im = (q • ↑r).im
repeat All goals completed! 🐙
@[simp, norm_cast]
lemma ofReal_qsmul (q : ℚ) (r : ℚ)
: ofRational (q • r) = q • r := q:ℚr:ℚ⊢ ↑(q • r) = q • ↑r
q:ℚr:ℚ⊢ (↑(q • r)).re = (q • ↑r).req:ℚr:ℚ⊢ (↑(q • r)).im = (q • ↑r).im
repeat All goals completed! 🐙
theorem conj_inv (x : ℚ[i]) : conj x⁻¹ = (conj x)⁻¹ := x:ℚ[i]⊢ (starRingEnd ℚ[i]) x⁻¹ = ((starRingEnd ℚ[i]) x)⁻¹
All goals completed! 🐙
@[simp, norm_cast]
theorem ofRational_div (r s : ℚ) : ((r / s : ℚ)
: ℚ[i]) = r / s :=
map_div₀ ofRational' r s
@[simp, norm_cast]
theorem ofReal_zpow (r : ℚ) (n : ℤ) : ((r ^ n : ℚ)
: ℚ[i]) = (r : ℚ[i]) ^ n :=
map_zpow₀ ofRational' r n
@[simp]
theorem div_I (z : ℚ[i]) : z / I = -(z * I) := z:ℚ[i]⊢ z / I = -(z * I)
z:ℚ[i]⊢ -(z * I) * I = z
z:ℚ[i]⊢ -(z * I * I) = z
calc
-(z * I * I) = -(z*(I*I)) := z:ℚ[i]⊢ -(z * I * I) = -(z * (I * I)) All goals completed! 🐙
_ = -(z*(-1)) := z:ℚ[i]⊢ -(z * (I * I)) = -(z * -1) All goals completed! 🐙
_ = z := z:ℚ[i]⊢ -(z * -1) = z All goals completed! 🐙
@[simp]
theorem inv_I : I⁻¹ = -I := ⊢ I⁻¹ = -I
All goals completed! 🐙
theorem normSq_inv (z : ℚ[i]) : normSq z⁻¹ = (normSq z)⁻¹:=
map_inv₀ normSq z
theorem normSq_div (z w : ℚ[i])
: normSq (z / w) = normSq z / normSq w :=
map_div₀ normSq z w
lemma div_ofRational (z : ℚ[i]) (x : ℚ)
: z / x = ⟨z.re / x, z.im / x⟩ := z:ℚ[i]x:ℚ⊢ z / ↑x = { re := z.re / x, im := z.im / x }
z:ℚ[i]x:ℚ⊢ (↑x)⁻¹ * z = { re := x⁻¹ * z.re, im := x⁻¹ * z.im }
z:ℚ[i]x:ℚ⊢ ((↑x)⁻¹ * z).re = { re := x⁻¹ * z.re, im := x⁻¹ * z.im }.re ∧
((↑x)⁻¹ * z).im = { re := x⁻¹ * z.re, im := x⁻¹ * z.im }.im
z:ℚ[i]x:ℚ⊢ (x / normSq ↑x = x⁻¹ ∨ z.re = 0) ∧ (x / normSq ↑x = x⁻¹ ∨ z.im = 0)
z:ℚ[i]x:ℚ⊢ x / normSq ↑x = x⁻¹ ∨ z.re = 0z:ℚ[i]x:ℚ⊢ x / normSq ↑x = x⁻¹ ∨ z.im = 0
repeat z:ℚ[i]x:ℚ⊢ x / normSq ↑x = x⁻¹ ; All goals completed! 🐙
lemma div_natCast (z : ℚ[i]) (n : ℕ)
: z / n = ⟨z.re / n, z.im / n⟩ :=
mod_cast div_ofRational z n
lemma div_intCast (z : ℚ[i]) (n : ℤ)
: z / n = ⟨z.re / n, z.im / n⟩ :=
mod_cast div_ofRational z n
lemma div_ratCast (z : ℚ[i]) (x : ℚ)
: z / x = ⟨z.re / x, z.im / x⟩ :=
mod_cast div_ofRational z x
lemma div_ofNat (z : ℚ[i]) (n : ℕ) [n.AtLeastTwo] :
z / OfNat.ofNat n
= ⟨z.re / OfNat.ofNat n, z.im / OfNat.ofNat n⟩ :=
div_natCast z n
@[simp] lemma div_ofReal_re (z : ℚ[i]) (x : ℚ)
: (z / x).re = z.re / x := z:ℚ[i]x:ℚ⊢ (z / ↑x).re = z.re / x
All goals completed! 🐙
@[simp] lemma div_ofReal_im (z : ℚ[i]) (x : ℚ)
: (z / x).im = z.im / x := z:ℚ[i]x:ℚ⊢ (z / ↑x).im = z.im / x
All goals completed! 🐙
@[simp] lemma div_natCast_re (z : ℚ[i]) (n : ℕ)
: (z / n).re = z.re / n := z:ℚ[i]n:ℕ⊢ (z / ↑n).re = z.re / ↑n
All goals completed! 🐙
@[simp] lemma div_natCast_im (z : ℚ[i]) (n : ℕ)
: (z / n).im = z.im / n := z:ℚ[i]n:ℕ⊢ (z / ↑n).im = z.im / ↑n
All goals completed! 🐙
@[simp] lemma div_intCast_re (z : ℚ[i]) (n : ℤ)
: (z / n).re = z.re / n := z:ℚ[i]n:ℤ⊢ (z / ↑n).re = z.re / ↑n
All goals completed! 🐙
@[simp] lemma div_intCast_im (z : ℚ[i]) (n : ℤ)
: (z / n).im = z.im / n := z:ℚ[i]n:ℤ⊢ (z / ↑n).im = z.im / ↑n
All goals completed! 🐙
@[simp] lemma div_ratCast_re (z : ℚ[i]) (x : ℚ)
: (z / x).re = z.re / x := z:ℚ[i]x:ℚ⊢ (z / ↑x).re = z.re / x
All goals completed! 🐙
@[simp] lemma div_ratCast_im (z : ℚ[i]) (x : ℚ)
: (z / x).im = z.im / x := z:ℚ[i]x:ℚ⊢ (z / ↑x).im = z.im / x
All goals completed! 🐙
@[simp]
lemma div_ofNat_re (z : ℚ[i]) (n : ℕ) [n.AtLeastTwo] :
(z / no_index (OfNat.ofNat n)).re
= z.re / OfNat.ofNat n
:= div_natCast_re z n
@[simp]
lemma div_ofNat_im (z : ℚ[i]) (n : ℕ) [n.AtLeastTwo] :
(z / no_index (OfNat.ofNat n)).im
= z.im / OfNat.ofNat n := div_natCast_im z n
We verify that this field has characteristic 0.
instance instCharZero : CharZero ℚ[i] :=
charZero_of_inj_zero fun n h => n:ℕh:↑n = 0⊢ n = 0
rwa [← ofRational_natCast, ofRational_eq_zero,
Nat.cast_eq_zeron:ℕh:n = 0⊢ n = 0 at h
Real and imaginary part can be computed using the usual formulas.
theorem re_eq_add_conj (z : ℚ[i])
: (z.re : ℚ) = (z + conj z) / 2 := z:ℚ[i]⊢ ↑z.re = (z + (starRingEnd ℚ[i]) z) / 2
z:ℚ[i]⊢ ↑z.re = ↑(2 * z.re) / 2
z:ℚ[i]⊢ ↑z.re = ↑2 * ↑z.re / 2
All goals completed! 🐙
-- Imaginary part of a complex number z equals the
-- difference of z and conj z divided by 2i
theorem im_eq_add_conj (z : ℚ[i])
: (z.im : ℚ) = (z - conj z) / (I*2) := z:ℚ[i]⊢ ↑z.im = (z - (starRingEnd ℚ[i]) z) / (I * 2)
z:ℚ[i]⊢ ↑z.im = ↑(2 * z.im) * I / (I * 2)
z:ℚ[i]⊢ ↑z.im = ↑2 * ↑z.im * I / (I * 2)
z:ℚ[i]⊢ ↑z.im = I * (↑2 * ↑z.im) / (I * 2)
z:ℚ[i]⊢ ↑z.im = I * ↑2 * ↑z.im / (I * 2)
z:ℚ[i]⊢ ↑z.im = I * 2 * ↑z.im / (I * 2)
z:ℚ[i]⊢ ↑z.im = ↑z.imz:ℚ[i]⊢ I * 2 ≠ 0
z:ℚ[i]⊢ ↑z.im = ↑z.im All goals completed! 🐙
z:ℚ[i]⊢ I * 2 ≠ 0 All goals completed! 🐙
Since our development for ℚ[i] is constructive, we can perform
explicit calculations. We can use Lean as a calculator of
complex numbers (with rational numbers as coordinates)
#eval 2*((2-I)*(2+I/6)/(I*5/3) + 5/2)
-- answer is 3 + -5*I
#eval normSq (2+2*I/4)*I*I
-- answer is (-17 : Rat)/4 + 0*I