mathlib3
e1feab4e - refactor(*): rename ordered groups/monoids to ordered add_ groups/monoids (#2347)

Commit
5 years ago
refactor(*): rename ordered groups/monoids to ordered add_ groups/monoids (#2347) In the perfectoid project we need ordered commutative monoids, and they are multiplicative. So the additive versions should be renamed to make some place.
Author
Parents
Loading