1.6. Ring structure
ℚ[i] is a communtative ring with identity.
instance commRing : CommRing ℚ[i] := {
addGroupWithOne with
mul := (· * ·)
npow := @npowRec _ ⟨(1 : ℚ[i])⟩ ⟨(· * ·)⟩
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✝).rea✝:ℚ[i]b✝:ℚ[i]⊢ (a✝ + b✝).im = (b✝ + a✝).im All goals completed! 🐙
left_distrib := ⊢ ∀ (a b c : ℚ[i]), a * (b + c) = a * b + a * c
a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝; a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝ * (b✝ + c✝)).re = (a✝ * b✝ + a✝ * c✝).rea✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝ * (b✝ + c✝)).im = (a✝ * b✝ + a✝ * c✝).im a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝ * (b✝ + c✝)).re = (a✝ * b✝ + a✝ * c✝).rea✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝ * (b✝ + c✝)).im = (a✝ * b✝ + a✝ * c✝).im a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ a✝.re * (b✝.im + c✝.im) + a✝.im * (b✝.re + c✝.re) = a✝.re * b✝.im + a✝.im * b✝.re + (a✝.re * c✝.im + a✝.im * c✝.re) a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ a✝.re * (b✝.re + c✝.re) - a✝.im * (b✝.im + c✝.im) = a✝.re * b✝.re - a✝.im * b✝.im + (a✝.re * c✝.re - a✝.im * c✝.im)a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ a✝.re * (b✝.im + c✝.im) + a✝.im * (b✝.re + c✝.re) = a✝.re * b✝.im + a✝.im * b✝.re + (a✝.re * c✝.im + a✝.im * c✝.re) All goals completed! 🐙
right_distrib := ⊢ ∀ (a b c : ℚ[i]), (a + b) * c = a * c + b * c
a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝; a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ ((a✝ + b✝) * c✝).re = (a✝ * c✝ + b✝ * c✝).rea✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ ((a✝ + b✝) * c✝).im = (a✝ * c✝ + b✝ * c✝).im a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ ((a✝ + b✝) * c✝).re = (a✝ * c✝ + b✝ * c✝).rea✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ ((a✝ + b✝) * c✝).im = (a✝ * c✝ + b✝ * c✝).im a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝.re + b✝.re) * c✝.im + (a✝.im + b✝.im) * c✝.re = a✝.re * c✝.im + a✝.im * c✝.re + (b✝.re * c✝.im + b✝.im * c✝.re) a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝.re + b✝.re) * c✝.re - (a✝.im + b✝.im) * c✝.im = a✝.re * c✝.re - a✝.im * c✝.im + (b✝.re * c✝.re - b✝.im * c✝.im)a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝.re + b✝.re) * c✝.im + (a✝.im + b✝.im) * c✝.re = a✝.re * c✝.im + a✝.im * c✝.re + (b✝.re * c✝.im + b✝.im * c✝.re) All goals completed! 🐙
zero_mul := ⊢ ∀ (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✝.re = 0 a✝:ℚ[i]⊢ 0 * a✝.re - 0 * a✝.im = 0a✝:ℚ[i]⊢ 0 * a✝.im + 0 * a✝.re = 0 All goals completed! 🐙
mul_zero := ⊢ ∀ (a : ℚ[i]), a * 0 = 0 a✝:ℚ[i]⊢ a✝ * 0 = 0; a✝:ℚ[i]⊢ (a✝ * 0).re = complexQ.re 0a✝:ℚ[i]⊢ (a✝ * 0).im = complexQ.im 0 a✝:ℚ[i]⊢ (a✝ * 0).re = complexQ.re 0a✝:ℚ[i]⊢ (a✝ * 0).im = complexQ.im 0 a✝:ℚ[i]⊢ a✝.re * 0 + a✝.im * 0 = 0 a✝:ℚ[i]⊢ a✝.re * 0 - a✝.im * 0 = 0a✝:ℚ[i]⊢ a✝.re * 0 + a✝.im * 0 = 0 All goals completed! 🐙
mul_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 a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.im + (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.re =
a✝.re * (b✝.re * c✝.im + b✝.im * c✝.re) + a✝.im * (b✝.re * c✝.re - b✝.im * c✝.im) a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.re - (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.im =
a✝.re * (b✝.re * c✝.re - b✝.im * c✝.im) - a✝.im * (b✝.re * c✝.im + b✝.im * c✝.re)a✝:ℚ[i]b✝:ℚ[i]c✝:ℚ[i]⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.im + (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.re =
a✝.re * (b✝.re * c✝.im + b✝.im * c✝.re) + a✝.im * (b✝.re * c✝.re - b✝.im * c✝.im) All goals completed! 🐙
one_mul := ⊢ ∀ (a : ℚ[i]), 1 * a = a
a✝:ℚ[i]⊢ 1 * a✝ = a✝;
a✝:ℚ[i]⊢ (1 * a✝).re = a✝.rea✝:ℚ[i]⊢ (1 * a✝).im = a✝.im a✝:ℚ[i]⊢ (1 * a✝).re = a✝.rea✝:ℚ[i]⊢ (1 * a✝).im = a✝.im All goals completed! 🐙
mul_one := ⊢ ∀ (a : ℚ[i]), a * 1 = a a✝:ℚ[i]⊢ a✝ * 1 = a✝; a✝:ℚ[i]⊢ (a✝ * 1).re = a✝.rea✝:ℚ[i]⊢ (a✝ * 1).im = a✝.im a✝:ℚ[i]⊢ (a✝ * 1).re = a✝.rea✝:ℚ[i]⊢ (a✝ * 1).im = a✝.im All goals completed! 🐙
mul_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✝).rea✝:ℚ[i]b✝:ℚ[i]⊢ (a✝ * b✝).im = (b✝ * a✝).im a✝:ℚ[i]b✝:ℚ[i]⊢ a✝.re * b✝.im + b✝.re * a✝.im = b✝.re * a✝.im + a✝.re * b✝.im; All goals completed! 🐙
}
instance : Ring ℚ[i] := ⊢ Ring ℚ[i] All goals completed! 🐙
instance : CommSemiring ℚ[i] := ⊢ CommSemiring ℚ[i] All goals completed! 🐙
instance : Semiring ℚ[i] := ⊢ Semiring ℚ[i] All goals completed! 🐙