Commit 2024-11-07 22:27 666dec72

feat(Combinatorics/Enumerative/Bell): number of ways of partitioning a set into subsets of given cardinalities (#15644)

• Multiset.bell m is the number of possibilities of dividing a set with m.sum elements into disjoint subsets with cardinalities indicated by m.
• Nat.uniformBell m n is Multiset.bell (replicate m n), the number of possibilities of dividing a set with m * n elements into m groups of n-element subsets These integers are defined as finite products of integers.
• Multiset.bell_eq shows that it equals some expression involving fractions of factorials, Multiset.bell_mul_eq shows the equivalent formula without division.
• Nat.uniformBell_eq shows that it equals (m * n).factorial / (m.factorial * n.factorial ^ m) and Nat.uniformBell_mul_factorial_mul_pow_factorial establishes the equality mchoose m n * m.factorial * n.factorial ^ m = (m * n).factorial.
• Nat.choose_mul_add and Nat.choose_mul_right are lemmas for Nat.choose that couldn't lie in Mathlib.Data.Nat.Choose.Basic because their proof uses the ring tactic. Co-authored with María Inés de Frutos-Fernández TODO : solve the enumerative problem.