Mathlib v3 is deprecated. Go to Mathlib v4

Theorem strict_anti_on.mul_antitone'

Modification history

2022-07-16 11:29
src/algebra/order/monoid_lemmas.lean
feat(algebra/order/monoid_lemmas): add `antitone`, `monotone_on`, and `antitone_on` lemmas (#15267)
Added strict_anti_on.mul_antitone'View on Github →