isPrimitiveClassified_of_coprime — Mathlib

English

If gcd x y = 1 for a Pythagorean triple, then h.IsPrimitiveClassified.

Русский

Если gcd(x,y)=1 для Пифагоровой тройки, то тройка примитивно классифицирована.

LaTeX

$$$\gcd(x,y) = 1 \Rightarrow h.IsPrimitiveClassified$$$

Lean4

theorem isPrimitiveClassified_of_coprime (hc : Int.gcd x y = 1) : h.IsPrimitiveClassified :=
  by
  by_cases hz : 0 < z
  · exact h.isPrimitiveClassified_of_coprime_of_pos hc hz
  have h' : PythagoreanTriple x y (-z) := by simpa [PythagoreanTriple, neg_mul_neg] using h.eq
  apply h'.isPrimitiveClassified_of_coprime_of_pos hc
  apply lt_of_le_of_ne _ (h'.ne_zero_of_coprime hc).symm
  exact le_neg.mp (not_lt.mp hz)

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