English
If a function f: M → G between a monoid M and a group G preserves multiplication (f(ab) = f(a)f(b) for all a,b), then there exists a monoid homomorphism from M to G whose underlying function is f.
Русский
Если функция f: M → G между моноидом M и группой G сохраняет умножение (для всех a,b выполняется f(ab) = f(a)f(b)), то существует моноид-гомоморфизм M → G, действующий как f на элементах.
LaTeX
$$$\\big( \\forall a,b\\in M,\ f(ab)=f(a)f(b) \\big) \\Rightarrow \\exists \\phi: M \\to^* G\\; (\\text{toFun}=f)$$$
Lean4
/-- Makes a group homomorphism from a proof that the map preserves multiplication. -/
@[to_additive (attr := simps -fullyApplied) /--
Makes an additive group homomorphism from a proof that the map preserves addition. -/
]
def mk' (f : M → G) (map_mul : ∀ a b : M, f (a * b) = f a * f b) : M →* G
where
toFun := f
map_mul' := map_mul
map_one' := by rw [← mul_right_cancel_iff, ← map_mul _ 1, one_mul, one_mul]
