Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-16 11:29 9becea2d

View on Github →

feat(algebra/order/monoid_lemmas_zero_lt): add some lemmas about typeclasses (#14761) ~~Rename some instances for consistency.~~ Some git messages are from the previous PR. Maybe it's because I performed some improper operations. I didn't find out the way to remove them. Sorry for that.

Estimated changes

Modified src/algebra/order/monoid_lemmas_zero_lt.lean

deleted theorem zero_lt.le_of_le_mul_of_le_one_right'

added theorem zero_lt.mul_pos_mono.to_mul_pos_reflect_lt

added theorem zero_lt.mul_pos_mono.to_mul_pos_strict_mono

added theorem zero_lt.mul_pos_mono_iff_mul_pos_reflect_lt

added theorem zero_lt.mul_pos_mono_iff_mul_pos_strict_mono

added theorem zero_lt.mul_pos_mono_rev.to_mul_pos_strict_mono

added theorem zero_lt.mul_pos_mono_rev_iff_mul_pos_reflect_lt

added theorem zero_lt.mul_pos_reflect_lt.to_mul_pos_mono

added theorem zero_lt.mul_pos_reflect_lt.to_mul_pos_mono_rev

added theorem zero_lt.mul_pos_strict_mono_iff_mul_pos_mono_rev

added theorem zero_lt.pos_mul_mono.to_pos_mul_reflect_lt

added theorem zero_lt.pos_mul_mono.to_pos_mul_strict_mono

added theorem zero_lt.pos_mul_mono_iff_mul_pos_mono

added theorem zero_lt.pos_mul_mono_iff_pos_mul_reflect_lt

added theorem zero_lt.pos_mul_mono_iff_pos_mul_strict_mono

added theorem zero_lt.pos_mul_mono_rev.to_pos_mul_strict_mono

added theorem zero_lt.pos_mul_mono_rev_iff_mul_pos_mono_rev

added theorem zero_lt.pos_mul_mono_rev_iff_pos_mul_reflect_lt

added theorem zero_lt.pos_mul_reflect_lt.to_pos_mul_mono

added theorem zero_lt.pos_mul_reflect_lt.to_pos_mul_mono_rev

added theorem zero_lt.pos_mul_reflect_lt_iff_mul_pos_reflect_lt

added theorem zero_lt.pos_mul_strict_mono_iff_mul_pos_strict_mono

added theorem zero_lt.pos_mul_strict_mono_iff_pos_mul_mono_rev

added theorem zero_lt.preorder.le_of_le_mul_of_le_one_right