mathlib

71b8c46a - feat(ring_theory/multiplicity): generalize `multiplicity` (#16330)

feat(ring_theory/multiplicity): generalize `multiplicity` (#16330) Divisibility is defined for any `semigroup`, so I also reduce the assumption of `multiplicity` to any `monoid`. At least it can be used for the elements which commute with every element, such as `power_series.X`. - [x] depends on: #16328