Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-25 19:52 666a2e2e

View on Github →

feat(algebra/group/with_one): more API for with_zero (#3716)

Estimated changes

Modified src/algebra/group/with_one.lean

added theorem with_one.some_eq_coe

Modified src/algebra/ordered_group.lean

added theorem with_zero.coe_le_coe

added theorem with_zero.coe_lt_coe

added theorem with_zero.lt_of_mul_lt_mul_left

added theorem with_zero.mul_le_mul_left

added theorem with_zero.zero_le

added theorem with_zero.zero_lt_coe

Modified src/analysis/calculus/times_cont_diff.lean

Modified src/analysis/mean_inequalities.lean

Modified src/topology/instances/ennreal.lean