inversion of a group with zero as a monoid_with_zero_hom?

Stream: Is there code for X?

[Michael Stoll]

If G is a comm_group_with_zero, then group_with_zero.inv : G → G is a monoid_with_zero_hom. Is this available in mathlib somewhere?

[Michael Stoll]

def inv_as_monoid_with_zero_hom {G : Type*} [comm_group_with_zero G] : G →*₀ G :=
{ to_fun := group_with_zero.inv, map_zero' := inv_zero, map_one' := inv_one,
  map_mul' := λ x y, mul_inv₀ }

[María Inés de Frutos Fernández]

Could you use docs#inv_monoid_with_zero_hom?