Multinomial theorem

Stream: Is there code for X?

[Pim Otte]

Does anyone know if the Multinomial theorem is in somewhere? I've tried searching for it, and I don't think so, but I could imagine it's somewhere under a different name, or in a more abstract way than I expect?

[Stuart Presnell]

I don't think it is. When I defined docs#nat.multichoose a few weeks ago it was suggested that I should make clear in the comments that this is not the multinomial, but no-one said "we have the multinomial theorem in mathlib, so you should link to it to demonstrate the difference".

[Yaël Dillies]

It's not in mathlib.