Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-16 11:53 32beebbc

View on Github →

feat(algebra/order/monoid): add simp lemmas (#12030)

Estimated changes

Modified src/algebra/order/monoid.lean

added theorem additive.of_mul_le

added theorem additive.of_mul_lt

added theorem additive.to_mul_le

added theorem additive.to_mul_lt

added theorem multiplicative.of_add_le

added theorem multiplicative.of_add_lt

added theorem multiplicative.to_add_le

added theorem multiplicative.to_add_lt