hom_map_lift

Mathlib.Algebra.FreeMonoid.Basic

URI: https://scilib.ai/kg/mathlib#FreeMonoid.hom_map_lift

← MathLib Explorer

English

For g: M →* N, f: α → M and x ∈ FreeMonoid α, g (lift f x) = lift (g ∘ f) x.

Русский

Для g: M →* N, f: α → M и x ∈ FreeMonoid α верно g (lift f x) = lift (g ∘ f) x.

LaTeX

$$$ g (lift\ f\ x) = lift\ (g \circ f)\ x $$$

Lean4

@[to_additive]
theorem hom_map_lift (g : M →* N) (f : α → M) (x : FreeMonoid α) : g (lift f x) = lift (g ∘ f) x :=
  DFunLike.ext_iff.1 (comp_lift g f) x

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru