Mathlib v3 is deprecated. Go to Mathlib v4

Theorem contravariant.mul_le_cancellable

Modification history

2021-08-18 21:30
src/algebra/ordered_monoid_lemmas.lean
feat(algebra/ordered_sub): define truncated subtraction in general (#8503) …
Added contravariant.mul_le_cancellableView on Github →