Mathlib v3 is deprecated. Go to Mathlib v4

Theorem strict_mono.mul'

Modification history

2021-10-01 13:24
src/algebra/order/monoid_lemmas.lean
feat(order/basic): Antitone functions (#9119) …
Modified strict_mono.mul'View on Github →
2021-07-30 02:40
src/algebra/ordered_monoid_lemmas.lean
feat(algebra/ordered_monoid_lemmas): add one `strict_mono` lemma and a few doc-strings (#8465) …
Added strict_mono.mul'View on Github →