mathlib
3afdf41f - chore(*): generalize some lemmas from `linear_ordered_semiring` to `ordered_semiring` (#5327)

Commit
5 years ago
chore(*): generalize some lemmas from `linear_ordered_semiring` to `ordered_semiring` (#5327) API changes: * Many lemmas now have weaker typeclass assumptions. Sometimes this means that `@myname _ _ _` needs one more `_`. * Drop `eq_one_of_mul_self_left_cancel` etc in favor of the new `mul_eq_left_iff` etc. * A few new lemmas that state `monotone` or `strict_mono_incr_on`.
Author
Parents
Loading