English
If f: M →* G is a monoid homomorphism to a commutative group G, then the inverse map f⁻¹: M →* G, defined by (f⁻¹)(x) = (f(x))⁻¹, is itself a monoid homomorphism.
Русский
Если f: M →* G — моноид-гомоморфизм в коммутативную группу G, то обратный гомоморфизм f⁻¹: M →* G, заданный (f⁻¹)(x) = (f(x))⁻¹, сам является моноид-гомоморфизмом.
LaTeX
$$$ (f)^{-1}(x) = f(x)^{-1} $$$
Lean4
/-- If `f` is a monoid homomorphism to a commutative group, then `f⁻¹` is the homomorphism sending
`x` to `(f x)⁻¹`. -/
@[to_additive /-- If `f` is an additive monoid homomorphism to an additive commutative group,
then `-f` is the homomorphism sending `x` to `-(f x)`. -/
]
instance : Inv (M →* G) where inv f := mk' (fun g ↦ (f g)⁻¹) fun a b ↦ by simp_rw [← mul_inv, f.map_mul]
