Commit 2025-09-05 17:21 7b3626cf

View on Github →

feat(RingTheory/DividedPowers/RatAlgebra): add definitions (#22322) In this file we show that, for certain choices of a commutative (semi)ring A and an ideal I of A, the family of maps ℕ → A → A given by fun n x ↦ x^n/n! is a divided power structure on I.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Nat/Factorial/NatCast.lean

added theorem Nat.castChoose_eq

Created Mathlib/RingTheory/DividedPowers/RatAlgebra.lean

added theorem DividedPowers.CharP.dpow_of_prime_le

added theorem DividedPowers.IsNilpotent.dpow_of_prime_le

added theorem DividedPowers.OfInvertibleFactorial.dpow_add

added theorem DividedPowers.OfInvertibleFactorial.dpow_add_of_lt

added theorem DividedPowers.OfInvertibleFactorial.dpow_apply

added theorem DividedPowers.OfInvertibleFactorial.dpow_comp

added theorem DividedPowers.OfInvertibleFactorial.dpow_comp_of_mul_lt

added theorem DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem

added theorem DividedPowers.OfInvertibleFactorial.dpow_eq_of_not_mem

added theorem DividedPowers.OfInvertibleFactorial.dpow_mem

added theorem DividedPowers.OfInvertibleFactorial.dpow_mul

added theorem DividedPowers.OfInvertibleFactorial.dpow_mul_of_add_lt

added theorem DividedPowers.OfInvertibleFactorial.dpow_null

added theorem DividedPowers.OfInvertibleFactorial.dpow_one

added theorem DividedPowers.OfInvertibleFactorial.dpow_zero

added theorem DividedPowers.OfInvertibleFactorial.mul_dpow

added theorem DividedPowers.OfSquareZero.dpow_of_two_le

added theorem DividedPowers.RatAlgebra.dividedPowers_unique

added theorem DividedPowers.RatAlgebra.dpow_apply

added theorem DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul

added theorem DividedPowers.RatAlgebra.dpow_eq_of_mem