Commit 2026-04-10 17:41 52cc3b45

feat(Data/Nat/Choose/Multinomial): multinomial coefficients (#35830) Define the multinomial coefficients, a variant of Nat.multinomial.

• redefine Multiset.multinomial. Given a multiset m of natural numbers, m.multinomial is the multinomial coefficient defined by (m.sum) ! / ∏ i ∈ m, m i !. As an example, Multiset.multinomial {1, 2, 2} = 30. This is the exponent of $x y^2 z^2$ in $(x+y+z)^5$. This should not be confused with the existing Multiset.multinomial which gives a different answer, for example, Multiset.multinomial {1, 2, 2} = 3. This function is renamed as Multiset.countPerms.
• Multiset.multinomial_cons proves that (x ::ₘ m).multinomial = Nat.choose (x + m.sum) x * m.multinomial
• Multiset.multinomial_add proves that (m + m').multinomial = Nat.choose (m + m').sum m.sum * m.multinomial * m'.multinomial co-authored with @mariainesdff