Theorem IsOrderedCancelMonoid.of_mul_lt_mul_left

Modification history

2025-10-09 12:15
Mathlib/Algebra/Order/Monoid/Defs.lean
feat(GroupTheory): add DivisibleHull (#29275) …
Added IsOrderedCancelMonoid.of_mul_lt_mul_leftView on Github →