Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-29 08:18 31297bda

View on Github →

refactor(algebra/order/with_zero): Generalize lemmas (#16240) Generalize the lemmas introduced in #15644 to monoids + covariant classes.

Estimated changes

deleted theorem eq_one_of_mul_eq_one_left