Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-05 11:38 54a2c6b6

View on Github →

chore(algebra/group/with_one): prove group_with_zero earlier, drop custom lemmas (#4385)

Estimated changes

modified theorem with_zero.coe_one
deleted theorem with_zero.div_eq_div
deleted theorem with_zero.div_mul_cancel
deleted theorem with_zero.div_one
deleted theorem with_zero.div_zero
deleted theorem with_zero.mul_comm
deleted theorem with_zero.mul_div_cancel
deleted theorem with_zero.mul_inv_cancel
deleted theorem with_zero.mul_inv_rev
deleted theorem with_zero.mul_left_inv
deleted theorem with_zero.mul_right_inv
deleted theorem with_zero.one_div
deleted theorem with_zero.zero_div
added theorem option.coe_def