mathlib3

ee189957 - feat(algebra/group_with_zero): `units.mk0` is a "monoid hom" (#8625)

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.