Commit 2024-01-06 18:06 8532fe9f

View on Github →

feat: define BinomialRing mixin (#6934) This file introduces the BinomialRing mixin (for semirings) and the Ring.multichoose function, which generalizes Nat.multichoose. These are preliminaries to introducing generalized binomial coefficients.

Estimated changes

modified theorem Commute.ofNat_left
modified theorem Commute.ofNat_right
modified theorem Nat.cast_comm
modified theorem Nat.cast_commute
modified theorem Nat.commute_cast
added def Ring.multichoose