Theorem Nat.Partition.powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted

Modification history

2025-12-05 16:31
Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean
feat(Combinatorics): Glaisher's theorem (#30618) …
Added Nat.Partition.powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestrictedView on Github →