mathlib3

0bef4a0b - feat(algebra/group_with_zero): pullback a `comm_cancel_monoid_with_zero` instance across an injective hom (#8515)

feat(algebra/group_with_zero): pullback a `comm_cancel_monoid_with_zero` instance across an injective hom (#8515) This generalizes `function.injective.cancel_monoid_with_zero` to the commutative case. See also: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/A.20submonoid.20of.20a.20.60cancel_monoid_with_zero.60.20also.20cancels