mathlib3

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

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