Commit 2025-12-05 16:31 6f5bfe86

View on Github →

feat(Combinatorics): Glaisher's theorem (#30618) This proves Glaisher's theorem, one of the 1000+ theorems. It is also a generalization of Euler's partition theorem, which can be rewritten as a collorary of this (will be in a different PR)

Estimated changes

Modified Archive/Wiedijk100Theorems/Partition.lean

Modified Mathlib.lean

Modified Mathlib/Combinatorics/Enumerative/Partition/Basic.lean

added def Nat.Partition.countRestricted

modified def Nat.Partition.distincts

modified def Nat.Partition.oddDistincts

modified def Nat.Partition.odds

added def Nat.Partition.restricted

Modified Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean

added theorem Nat.Partition.tendsto_order_genFun_term_atTop_nhds_top

Created Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean

added theorem Nat.Partition.card_restricted_eq_card_countRestricted

added theorem Nat.Partition.hasProd_powerSeriesMk_card_countRestricted

added theorem Nat.Partition.hasProd_powerSeriesMk_card_restricted

added theorem Nat.Partition.multipliable_powerSeriesMk_card_countRestricted

added theorem Nat.Partition.multipliable_powerSeriesMk_card_restricted

added theorem Nat.Partition.powerSeriesMk_card_countRestricted_eq_tprod

added theorem Nat.Partition.powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted

added theorem Nat.Partition.powerSeriesMk_card_restricted_eq_tprod

Modified Mathlib/RingTheory/PowerSeries/PiTopology.lean

added theorem PowerSeries.WithPiTopology.multipliable_one_sub_X_pow

added theorem PowerSeries.WithPiTopology.tprod_one_sub_X_pow_ne_zero

Modified docs/1000.yaml