Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-10 12:28 699c9153

View on Github →

feat(number_theory): pythagorean triples (#3200) The classification of pythagorean triples (one of the "100 theorems")

Estimated changes

added theorem int.exists_gcd_one'
added theorem int.exists_gcd_one
added theorem int.ne_zero_of_gcd
added theorem int.pow_dvd_pow_iff
added theorem int.prime.dvd_mul'
added theorem int.prime.dvd_mul
added theorem pow_dvd_pow_of_dvd
added theorem pow_two_pos_of_ne_zero
added theorem pow_two_sub_pow_two
added theorem int.sub_mod
added theorem rat.div_int_inj
added theorem circle_equiv_apply
added def circle_equiv_gen
added theorem pythagorean_triple.eq
added theorem pythagorean_triple.mul