English
If k ≠ 0, scaling preserves being a Pythagorean triple in both directions: PythagoreanTriple(kx,ky,kz) ⇔ PythagoreanTriple(x,y,z).
Русский
Если k ≠ 0, масштабирование сохраняет Пифагорову тройку в обе стороны: PythagoreanTriple(kx,ky,kz) ⇔ PythagoreanTriple(x,y,z).
LaTeX
$$k \neq 0 \Rightarrow \big(PythagoreanTriple(kx,ky,kz) \iff PythagoreanTriple(x,y,z)\big)$$
Lean4
/-- `(k*x, k*y, k*z)` is a Pythagorean triple if and only if
`(x, y, z)` is also a triple. -/
theorem mul_iff (k : ℤ) (hk : k ≠ 0) : PythagoreanTriple (k * x) (k * y) (k * z) ↔ PythagoreanTriple x y z :=
by
refine ⟨?_, fun h => h.mul k⟩
simp only [PythagoreanTriple]
intro h
rw [← mul_left_inj' (mul_ne_zero hk hk)]
convert h using 1 <;> ring
