coe_compAddChar

Mathlib.Algebra.Group.AddChar

URI: https://scilib.ai/kg/mathlib#MonoidHom.coe_compAddChar

← MathLib Explorer

English

The action of the composed map on an input a is the same as applying φ to a and then f: (ψ ∘ f)(a) = ψ(f(a)).

Русский

Разбор применения составленного отображения: (ψ ∘ f)(a) = ψ(f(a)).

LaTeX

$$$$ (\psi \circ f)(a) = \psi(f(a)). $$$$

Lean4

@[simp, norm_cast]
theorem _root_.MonoidHom.coe_compAddChar {N : Type*} [Monoid N] (f : M →* N) (φ : AddChar A M) :
    f.compAddChar φ = f ∘ φ :=
  rfl

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

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

Разделы

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

Аффилиация

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