Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-28 17:20 e6a3ca81

View on Github →

refactor(algebra/group): generalise and extend the API for with_zero (#762)

  • refactor(algebra/group): generalise and extend the API for with_zero
  • Shorter proof. Thanks Chris
  • Travis, try your best

Estimated changes

added theorem with_one.coe_inj
added theorem with_one.coe_ne_one
added theorem with_one.mul_coe
added theorem with_one.one_ne_coe
added theorem with_zero.coe_one
added theorem with_zero.div_coe
added theorem with_zero.div_eq_div
added theorem with_zero.div_one
added theorem with_zero.div_zero
added theorem with_zero.inv_coe
added theorem with_zero.inv_one
added theorem with_zero.inv_zero
added theorem with_zero.mul_coe
added theorem with_zero.mul_inv_rev
added theorem with_zero.mul_left_inv
added theorem with_zero.one_div
added theorem with_zero.zero_div