Theorems · Theorem · number theory

PythagoreanTriple.isPrimitiveClassified_aux

∀ {x y z : ℤ} (h : PythagoreanTriple x y z),
  x.gcd y = 1 →
    0 < z →
      ∀ {m n : ℤ},
        0 < m ^ 2 + n ^ 2 →
          ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2) →
            ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2) →
              (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1 →
                m.gcd n = 1 → m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0 → h.IsPrimitiveClassified

Defined in: Mathlib.NumberTheory.PythagoreanTriples
Cited by: 1 results in Mathlib
Foundations: Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

ne_of_gtproof · cited by 637
Int.cast_ofNatproof · cited by 86
PythagoreanTriplestatement and proof · cited by 24
div_left_inj'proof · cited by 11
PythagoreanTriple.IsPrimitiveClassifiedstatement · cited by 7
PythagoreanTriple.coprime_of_coprimeproof · cited by 2
Rat.div_int_injproof · cited by 2

Cited by1

Results whose statement or proof uses this declaration.

PythagoreanTriple.isPrimitiveClassified_of_coprime_of_odd_of_posproof · cited by 1