Commit 2022-05-12 12:10 d9e623c2

feat(algebra/*): Division monoid instances for with_zero and mul_opposite (#14073) A few missing instances of division_monoid and friends.

added theorem inv_comp_inv

modified theorem with_zero.coe_inv