Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-30 11:09 58f8817e

View on Github →

feat(number_theory/fermat4): The n=4 case of fermat (#4720) Fermat's last theorem for n=4.

Estimated changes

Modified src/algebra/gcd_monoid.lean

modified theorem exists_associated_pow_of_mul_eq_pow

Modified src/algebra/group_power/lemmas.lean

added theorem int.abs_le_self_pow_two

added theorem int.le_self_pow_two

Modified src/algebra/group_with_zero_power.lean

added theorem ne_zero_pow

modified theorem pow_eq_zero'

modified theorem pow_ne_zero'

modified theorem zero_pow'

modified theorem zero_pow_eq_zero

Modified src/data/int/basic.lean

added theorem int.neg_mod_two

Created src/number_theory/fermat4.lean

added theorem fermat_42.comm

added theorem fermat_42.coprime_of_minimal

added theorem fermat_42.exists_minimal

added theorem fermat_42.exists_odd_minimal

added theorem fermat_42.exists_pos_odd_minimal

added def fermat_42.minimal

added theorem fermat_42.minimal_comm

added theorem fermat_42.mul

added theorem fermat_42.ne_zero

added theorem fermat_42.neg_of_minimal

added theorem fermat_42.not_minimal

added def fermat_42

added theorem int.coprime_of_sqr_sum'

added theorem int.coprime_of_sqr_sum

added theorem not_fermat_42

added theorem not_fermat_4

Modified src/number_theory/pythagorean_triples.lean

added theorem pythagorean_triple.coprime_classification'

Modified src/ring_theory/int/basic.lean

added theorem int.exists_unit_of_abs

added theorem int.gcd_eq_one_iff_coprime

added theorem int.prime.dvd_pow'

added theorem int.prime.dvd_pow

added theorem int.sqr_of_coprime

added theorem int.sqr_of_gcd_eq_one