Commit 2025-08-24 17:49 904df448

View on Github →

feat: x - 1 ∣ x ^ n - 1 for Nat (#28788)

Estimated changes

Modified Mathlib/Algebra/Ring/GeomSum.lean

modified theorem Nat.geomSum_eq

added theorem Nat.pow_sub_one_dvd_pow_sub_one

added theorem Nat.pow_sub_pow_dvd_pow_sub_pow

added theorem Nat.sub_one_dvd_pow_sub_one

modified theorem Odd.nat_add_dvd_pow_add_pow

deleted theorem nat_pow_one_sub_dvd_pow_mul_sub_one

deleted theorem nat_sub_dvd_pow_sub_pow

Modified Mathlib/NumberTheory/Fermat.lean

Modified Mathlib/NumberTheory/FermatPsp.lean