mul — Mathlib

English

If (x,y,z) is a Pythagorean triple, then for any integer k, (k x, k y, k z) is also a Pythagorean triple.

Русский

Если (x,y,z) — Пифагова тройка, то для любого целого k тройка (k x, k y, k z) тоже является Пифагоровой тройкой.

LaTeX

$$$PythagoreanTriple(x,y,z) \Rightarrow PythagoreanTriple(kx,ky,kz)$$$

Lean4

/-- A triple is still a triple if you multiply `x`, `y` and `z`
by a constant `k`. -/
theorem mul (h : PythagoreanTriple x y z) (k : ℤ) : PythagoreanTriple (k * x) (k * y) (k * z) :=
  calc
    k * x * (k * x) + k * y * (k * y) = k ^ 2 * (x * x + y * y) := by ring
    _ = k ^ 2 * (z * z) := by rw [h.eq]
    _ = k * z * (k * z) := by ring

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