mathlib

222faeda - feat(algebra/group/units_hom): make `is_unit.map` work on `monoid_hom_class` (#12577)

feat(algebra/group/units_hom): make `is_unit.map` work on `monoid_hom_class` (#12577) `ring_hom.is_unit_map` and `mv_power_series.is_unit_constant_coeff` are now redundant, but to keep this diff small I've left them around.