English
Dividing the coordinates by gcd(x,y) yields another Pythagorean triple.
Русский
Разделяя координаты на НОД(x,y), получаем другую Пифагорову тройку.
LaTeX
$$$PythagoreanTriple(x,y,z) \Rightarrow PythagoreanTriple\left(\frac{x}{\gcd(x,y)}, \frac{y}{\gcd(x,y)}, \frac{z}{\gcd(x,y)}\right)$$$
Lean4
theorem normalize : PythagoreanTriple (x / Int.gcd x y) (y / Int.gcd x y) (z / Int.gcd x y) :=
by
by_cases h0 : Int.gcd x y = 0
· have hx : x = 0 := by
apply Int.natAbs_eq_zero.mp
apply Nat.eq_zero_of_gcd_eq_zero_left h0
have hy : y = 0 := by
apply Int.natAbs_eq_zero.mp
apply Nat.eq_zero_of_gcd_eq_zero_right h0
have hz : z = 0 := by simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero, or_self_iff] using h
simp only [hx, hy, hz]
exact zero
rcases h.gcd_dvd with ⟨z0, rfl⟩
obtain ⟨k, x0, y0, k0, h2, rfl, rfl⟩ : ∃ (k : ℕ) (x0 y0 : _), 0 < k ∧ Int.gcd x0 y0 = 1 ∧ x = x0 * k ∧ y = y0 * k :=
Int.exists_gcd_one' (Nat.pos_of_ne_zero h0)
have hk : (k : ℤ) ≠ 0 := by
norm_cast
rwa [pos_iff_ne_zero] at k0
rw [Int.gcd_mul_right, h2, Int.natAbs_natCast, one_mul] at h ⊢
rw [mul_comm x0, mul_comm y0, mul_iff k hk] at h
rwa [Int.mul_ediv_cancel _ hk, Int.mul_ediv_cancel _ hk, Int.mul_ediv_cancel_left _ hk]
