Commit 2023-03-23 14:22 ab3732ff

View on Github →

feat: port NumberTheory.PythagoreanTriples (#3022)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/PythagoreanTriples.lean

added theorem Int.sq_ne_two_mod_four

added def PythagoreanTriple.IsClassified

added def PythagoreanTriple.IsPrimitiveClassified

added theorem PythagoreanTriple.classification

added theorem PythagoreanTriple.classified

added theorem PythagoreanTriple.coprime_classification'

added theorem PythagoreanTriple.coprime_classification

added theorem PythagoreanTriple.coprime_of_coprime

added theorem PythagoreanTriple.eq

added theorem PythagoreanTriple.even_odd_of_coprime

added theorem PythagoreanTriple.gcd_dvd

added theorem PythagoreanTriple.isClassified_of_isPrimitiveClassified

added theorem PythagoreanTriple.isClassified_of_normalize_isPrimitiveClassified

added theorem PythagoreanTriple.isPrimitiveClassified_aux

added theorem PythagoreanTriple.isPrimitiveClassified_of_coprime

added theorem PythagoreanTriple.isPrimitiveClassified_of_coprime_of_odd_of_pos

added theorem PythagoreanTriple.isPrimitiveClassified_of_coprime_of_pos

added theorem PythagoreanTriple.isPrimitiveClassified_of_coprime_of_zero_left

added theorem PythagoreanTriple.mul

added theorem PythagoreanTriple.mul_iff

added theorem PythagoreanTriple.mul_isClassified

added theorem PythagoreanTriple.ne_zero_of_coprime

added theorem PythagoreanTriple.normalize

added theorem PythagoreanTriple.symm

added theorem PythagoreanTriple.zero

added def PythagoreanTriple

added def circleEquivGen

added theorem circle_equiv_apply

added theorem circle_equiv_symm_apply

added theorem pythagoreanTriple_comm

added theorem sq_ne_two_fin_zMod_four