Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-22 04:56 83db96b2

View on Github →

feat(algebra/group/with_one): make with_one and with_zero irreducible. (#3883)

Estimated changes

added theorem with_one.coe_mul
deleted theorem with_one.mul_coe
added theorem with_zero.coe_inv
added theorem with_zero.coe_mul
deleted theorem with_zero.inv_coe
deleted theorem with_zero.mul_coe
added theorem with_zero.mul_comm
added theorem with_zero.mul_zero
added theorem with_zero.zero_mul