Commit 2025-11-15 20:48 b8d4bc69

feat(Combinatorics): generating function for partitions (#30567) This is the start of a series of PR aiming to prove two theorems related to partition:

• Glaisher's theorem, which is a generalization of the existing Euler's Partition theorem. The proof will use the infinite generating function, upgrading the current proof that uses finite ones, and resolving this TODO
• Pentagonal number theorem and the recurrence relation on the partition function.

I created a new file Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean to avoid importing PowerSeries stuff directly into the definition file, and along the way I moved the existing Mathlib/Combinatorics/Enumerative/Partition.lean to Mathlib/Combinatorics/Enumerative/Partition/Basic.lean .