Theorems · Theorem · number theory

PythagoreanTriple.classification

• #23 of the 100 theorems: Formula for Pythagorean Triples

∀ {x y z : ℤ},
  PythagoreanTriple x y z ↔
    ∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Formula for Pythagorean Triples

Defined in

Mathlib.NumberTheory.PythagoreanTriples

Cited by

0 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound