English
There is a unique monoid homomorphism map f: FreeMonoid α →* FreeMonoid β sending each of x to of (f x).
Русский
Существует единственный моноид-гомоморфизм map f: FreeMonoid α →* FreeMonoid β, отправляющий each of x в of (f x).
LaTeX
$$$ FreeMonoid.map\ f: FreeMonoid\alpha \to^* FreeMonoid\beta $$$
Lean4
/-- The unique monoid homomorphism `FreeMonoid α →* FreeMonoid β` that sends
each `of x` to `of (f x)`. -/
@[to_additive /-- The unique additive monoid homomorphism `FreeAddMonoid α →+ FreeAddMonoid β`
that sends each `of x` to `of (f x)`. -/
]
def map (f : α → β) : FreeMonoid α →* FreeMonoid β
where
toFun l := ofList <| l.toList.map f
map_one' := rfl
map_mul' _ _ := List.map_append
