Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-14 16:17 71b8c46a

View on Github →

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.

Estimated changes