Commit 2024-10-11 15:01 85cf1f19

View on Github →

chore(NumberTheory/Fermat): rename fermat to Nat.fermatNumber (#17618) (And also namespace and rename the lemmas about them.) As discussed in the reviewers chatroom.

Estimated changes

Modified Mathlib/NumberTheory/Fermat.lean

added theorem Nat.coprime_fermatNumber_fermatNumber

added def Nat.fermatNumber

added theorem Nat.fermatNumber_eq_prod_add_two

added theorem Nat.fermatNumber_one

added theorem Nat.fermatNumber_product

added theorem Nat.fermatNumber_two

added theorem Nat.fermatNumber_zero

added theorem Nat.odd_fermatNumber

added theorem Nat.strictMono_fermatNumber

added theorem Nat.two_lt_fermatNumber

deleted theorem coprime_fermat_fermat

deleted def fermat

deleted theorem fermat_eq_prod_add_two

deleted theorem fermat_one

deleted theorem fermat_product

deleted theorem fermat_two

deleted theorem fermat_zero

deleted theorem odd_fermat

deleted theorem strictMono_fermat

deleted theorem two_lt_fermat