English
If f and g are monoid homomorphisms to a commutative group G, then the division f / g defined by x ↦ f(x) / g(x) is again a monoid homomorphism.
Русский
Если f и g — гомоморфизмы моноидов в коммутативную группу G, то деление f / g, определяемое по формуле x ↦ f(x) / g(x), снова является гомоморфизмом моноидов.
LaTeX
$$$ (f / g)(x) = f(x) / g(x) $$$
Lean4
/-- If `f` and `g` are monoid homomorphisms to a commutative group, then `f / g` is the homomorphism
sending `x` to `(f x) / (g x)`. -/
@[to_additive /-- If `f` and `g` are monoid homomorphisms to an additive commutative group,
then `f - g` is the homomorphism sending `x` to `(f x) - (g x)`. -/
]
instance : Div (M →* G) where
div f g := mk' (fun x ↦ f x / g x) fun a b ↦ by simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]
