Commit 2023-03-24 11:47 ebf7fac2

View on Github →

feat: port NumberTheory.Fermat4 (#3064)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Fermat4.lean

added def Fermat42.Minimal

added theorem Fermat42.comm

added theorem Fermat42.coprime_of_minimal

added theorem Fermat42.exists_minimal

added theorem Fermat42.exists_odd_minimal

added theorem Fermat42.exists_pos_odd_minimal

added theorem Fermat42.minimal_comm

added theorem Fermat42.mul

added theorem Fermat42.ne_zero

added theorem Fermat42.neg_of_minimal

added theorem Fermat42.not_minimal

added def Fermat42

added theorem Int.coprime_of_sq_sum'

added theorem Int.coprime_of_sq_sum

added theorem not_fermat_42

added theorem not_fermat_4