lift_apply — Mathlib

English

There is a canonical monoid homomorphism map f: FreeMonoid α →* FreeMonoid β that sends each generator of α to its image under f and extends uniquely to a monoid homomorphism.

Русский

Существует канонический моноид-гомоморфизм map f: FreeMonoid α →* FreeMonoid β, отправляющий каждый порождающий элемент α в его образ под f и единственным образом продолжающийся до гомоморфизма моноидов.

LaTeX

$$$ FreeMonoid.map\ f: FreeMonoid\alpha \to^* FreeMonoid\beta $$$

Lean4

@[to_additive]
theorem lift_apply (f : α → M) (l : FreeMonoid α) : lift f l = ((toList l).map f).prod :=
  prodAux_eq _

Похожие утверждения