Commit 2021-08-12 15:02 ee189957

feat(algebra/group_with_zero): units.mk0 is a "monoid hom" (#8625) This PR shows that units.mk0 sends 1 to 1 and x * y to mk0 x * mk0 y. So it is a monoid hom, if we ignore the proof fields.