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
.
- depends on: #16328