divides_sq_eq_zero_z — Mathlib

English

If x, y ∈ ℤ and x^2 = d y^2 with d nonsquare, then x = 0 and y = 0.

Русский

Если x^2 = d y^2 для целых x, y и d ненквадратное, то x = 0 и y = 0.

LaTeX

$$$$\forall d \in \mathbb{N},\; [\text{Nonsquare}(d)]\Rightarrow \forall x,y \in \mathbb{Z},\; x^2 = d y^2 \Rightarrow x=0 \land y=0.$$$$

Lean4

theorem divides_sq_eq_zero_z {x y : ℤ} (h : x * x = d * y * y) : x = 0 ∧ y = 0 :=
  by
  rw [mul_assoc, ← Int.natAbs_mul_self, ← Int.natAbs_mul_self, ← Int.natCast_mul, ← mul_assoc] at h
  exact
    let ⟨h1, h2⟩ := divides_sq_eq_zero (Int.ofNat.inj h)
    ⟨Int.natAbs_eq_zero.mp h1, Int.natAbs_eq_zero.mp h2⟩

Похожие утверждения