English
For a,b ∈ Z√d with a*b = 0, either a = 0 or b = 0 (under nonsquare d).
Русский
Для a,b ∈ Z√d при a*b = 0 либо a = 0, либо b = 0 (при ненквадратном d).
LaTeX
$$$$\forall a,b \in \mathbb{Z}\sqrt{d},\; a b = 0 \Rightarrow a = 0 \lor b = 0.$$$$
Lean4
protected theorem eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : ℤ√d}, a * b = 0 → a = 0 ∨ b = 0
| ⟨x, y⟩, ⟨z, w⟩, h => by
injection h with h1 h2
have h1 : x * z = -(d * y * w) := eq_neg_of_add_eq_zero_left h1
have h2 : x * w = -(y * z) := eq_neg_of_add_eq_zero_left h2
have fin : x * x = d * y * y → (⟨x, y⟩ : ℤ√d) = 0 := fun e =>
match x, y, divides_sq_eq_zero_z e with
| _, _, ⟨rfl, rfl⟩ => rfl
exact
if z0 : z = 0 then
if w0 : w = 0 then
Or.inr
(match z, w, z0, w0 with
| _, _, rfl, rfl => rfl)
else
Or.inl <|
fin <|
mul_right_cancel₀ w0 <|
calc
x * x * w = -y * (x * z) := by simp [h2, mul_assoc, mul_left_comm]
_ = d * y * y * w := by simp [h1, mul_assoc, mul_left_comm]
else
Or.inl <|
fin <|
mul_right_cancel₀ z0 <|
calc
x * x * z = d * -y * (x * w) := by simp [h1, mul_assoc, mul_left_comm]
_ = d * y * y * z := by simp [h2, mul_assoc, mul_left_comm]
