Commit 2024-11-27 09:56 8674145a

View on Github →

chore(NumberTheory/Fermat): fix theorem names (#19469) From LeanCamCombi

Estimated changes

Modified Mathlib/NumberTheory/Fermat.lean

modified theorem Nat.coprime_fermatNumber_fermatNumber

added theorem Nat.fermatNumber_injective

added theorem Nat.fermatNumber_mono

added theorem Nat.fermatNumber_ne_one

deleted theorem Nat.fermatNumber_product

added theorem Nat.fermatNumber_strictMono

added theorem Nat.pairwise_coprime_fermatNumber

added theorem Nat.prod_fermatNumber

deleted theorem Nat.strictMono_fermatNumber

added theorem Nat.three_le_fermatNumber

modified theorem Nat.two_lt_fermatNumber