Replace Nat.multichoose with Ring.multichoose?

Stream: mathlib4

[Scott Carnahan]

In a comment attached to #6934, @Yaël Dillies suggested eventually replacing Nat.multichoose with Ring.multichoose. I tried in in a branch back in December 2023, and the main effect was the addition of Mathlib.RingTheory.Binomial as an import to Mathlib.Data.List.Sym (along with some minor alterations to proofs). Is that considered an acceptable cost?

[Kyle Miller]

My gut feeling is that it's good to keep a "low-brow" definition, especially if it keeps imports low. Instead, we could have simp lemmas that transform the Nat definition into the general Ring one. Happy to hear other opinions.

[Yaël Dillies]

With my sublibrary carver hat (a pretty recent hat!) on, I must say that docs#Nat.multichoose is actually pretty close to being eligible for Std, so I want to retract my previous statement and claim that actually it's fine/better to have both

[Scott Carnahan]

Thank you. I'm glad I asked here.

[Eric Wieser]

Is the answer here to have a HasMultichoose typeclass?

[Eric Wieser]

That way we don't have to rewrite between the definitions

[Eric Wieser]

(and this is just a base class of the docs#BinomialRing typeclass we already have)