Theorem Nat.Partition.card_odds_eq_card_distincts

Modification history

2025-12-11 00:09
Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean
refactor: re-prove Euler's partition theorem from Glaisher's theorem (#31873) …
Added Nat.Partition.card_odds_eq_card_distinctsView on Github →