Theorems · Definition · number theory
PythagoreanTriple.IsPrimitiveClassified
{x y z : ℤ} → PythagoreanTriple x y z → PropA primitive Pythagorean triple x, y, z is a Pythagorean triple with x and y coprime.
Such a triple is “primitively classified” if there exist coprime integers m, n such that either
* x = m ^ 2 - n ^ 2 and y = 2 * m * n, or
* x = 2 * m * n and y = m ^ 2 - n ^ 2.
- Defined in
- Mathlib.NumberTheory.PythagoreanTriples
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PythagoreanTriplestatement and proof · cited by 24
Cited by7
Results whose statement or proof uses this declaration.
- PythagoreanTriple.isPrimitiveClassified_of_coprimestatement · cited by 2
- PythagoreanTriple.isClassified_of_isPrimitiveClassifiedstatement and proof · cited by 1
- PythagoreanTriple.isClassified_of_normalize_isPrimitiveClassifiedstatement and proof · cited by 1
- PythagoreanTriple.isPrimitiveClassified_auxstatement · cited by 1
- PythagoreanTriple.isPrimitiveClassified_of_coprime_of_odd_of_posstatement · cited by 1
- PythagoreanTriple.isPrimitiveClassified_of_coprime_of_posstatement · cited by 1
- PythagoreanTriple.isPrimitiveClassified_of_coprime_of_zero_leftstatement · cited by 1