English
The map prod : FreeGroup α →* α is the unique homomorphism extending the identity on α, defined as lift id.
Русский
Пусть prod : FreeGroup α →* α — единственный гомоморфизм, который распространяет тождественный отображение на α; он задаётся как lift id.
LaTeX
$$$ \\mathrm{prod} : \\mathrm{FreeGroup}\\ α \\to^* α \\quad\\text{and}\\quad prod = \\mathrm{lift}\\ id $$$
Lean4
/-- If `α` is a group, then any function from `α` to `α` extends uniquely to a homomorphism from the
free group over `α` to `α`. This is the multiplicative version of `FreeGroup.sum`. -/
@[to_additive /-- If `α` is an additive group, then any function from `α` to `α` extends uniquely
to an additive homomorphism from the additive free group over `α` to `α`. -/
]
def prod : FreeGroup α →* α :=
lift id
