English
Let f: α → β. The induced map on free groups, denoted by f̂, preserves multiplication: for all x,y in FreeGroup(α), f̂(xy) = f̂(x) f̂(y). In other words, the image map is a group homomorphism.
Русский
Пусть f: α → β. Индукционное отображение на свободной группе, обозначаемое как f̂, сохраняет умножение: для любых x,y ∈ FreeGroup(α) выполняется f̂(xy) = f̂(x) f̂(y). Иными словами, изображение является гомоморфизмом группы.
LaTeX
$$$$\\forall f:\\alpha \\to \\beta,\\ \\forall x,y\\in \\mathrm{FreeGroup}(\\alpha),\\ \\widehat{f}(xy)=\\widehat{f}(x)\\widehat{f}(y).$$$$
Lean4
@[to_additive (attr := simp)]
theorem map_mul (f : α → β) (x y : FreeGroup α) : f <$> (x * y) = f <$> x * f <$> y :=
(map f).map_mul x y
