Multinomial coefficients

Stream: mathlib4

[Antoine Chambert-Loir]

Multinomial coefficients are defined in mathlib by docs#Nat.multinomial, that constructs $(\sum_{i\in s} a_i)!/\prod_{i\in s} a_i!$, for some $\mathbf N$-valued function $a$, and some finite set $s$.

In our work on divided powers, @María Inés de Frutos Fernández and fI need to access multinomial coefficients so that the multinomial number associated with the set $\{1,2,2\}$ of natural numbers is $5!/1!2!2! = 30$.

We develop that notion in #35830 but reached a name-conflict since docs#Multiset.multinomial already exists, and gives $3$ in that case.
Our solution has been to name our coefficients Multiset.plurinomial, trading a Greek root for a Latine one.

However, in their review, @Violeta Hernández suggested that we'd rather name our coefficients Multiset.plurinomial and rename docs#Multiset.multinomial as Multiset.countPerms. — Indeed, it counts the number of lists that give rise to the given multiset.

We're of course ready to do that change but felt natural to have a more general discussion here.

[Bolton Bailey]

I also think this would be a great change, I have an old incomplete draft PR doing this #31601 (the main motivation of that PR being a version of docs#Nat.choose with an easy positivity plugin), feel free to steal lemmas from that if needed.

In my PR I named this function Nat.multinomial', which I think tells me that this is the function I expected "multinomial" to name, and so I think this renaming is appropriate.