Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-31 06:51 81c5d17e

View on Github →

chore(algebra/order/monoid_lemmas): remove exactly same lemmas (#13068)

Estimated changes

modified theorem mul_lt_of_lt_of_lt_one
modified theorem mul_lt_of_lt_one_of_lt