mathlib3

bd12701e - feat(algebra/group_with_zero): add `eq_on_inv₀` (#16222)

feat(algebra/group_with_zero): add `eq_on_inv₀` (#16222) * move some lemmas up in the import chain; * use `namespace is_unit`; * add `is_unit.eq_on_inv` and `eq_on_inv₀`; * rename `monoid_hom.eq_on_inv` to `eq_on_inv`, make `f` and `g` explicit.