Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-16 19:44 e763499b

View on Github →

chore(algebra/order/monoid_lemmas_zero_lt): remove redundant assumptions (#16524) The third part of #16449

Estimated changes

Modified src/algebra/order/monoid_lemmas_zero_lt.lean

modified theorem mul_pos_mono_iff_mul_pos_reflect_lt

modified theorem mul_pos_reflect_lt.to_mul_pos_mono

modified theorem pos_mul_mono_iff_pos_mul_reflect_lt

modified theorem pos_mul_reflect_lt.to_pos_mul_mono