Commit 2024-10-10 16:52 f2f74496

View on Github →

Revert "chore(NumberTheory/Fermat): rename fermat to Nat.fermatNumber" This reverts commit a2862c2cb9d46533bf32565583ed9c9f6fd300b6.

Estimated changes

deleted def Nat.fermatNumber
deleted theorem Nat.fermatNumber_one
deleted theorem Nat.fermatNumber_product
deleted theorem Nat.fermatNumber_two
deleted theorem Nat.fermatNumber_zero
deleted theorem Nat.odd_fermatNumber
deleted theorem Nat.two_lt_fermatNumber
added theorem coprime_fermat_fermat
added def fermat
added theorem fermat_eq_prod_add_two
added theorem fermat_one
added theorem fermat_product
added theorem fermat_two
added theorem fermat_zero
added theorem odd_fermat
added theorem strictMono_fermat
added theorem two_lt_fermat