coe_comp

Mathlib.Algebra.Algebra.NonUnitalHom

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgHom.coe_comp

English

The underlying function of the composite equals the composition of the underlying functions.

Русский

Базовая функция композиции равна композиции базовых функций.

LaTeX

$$$\text{coe}(f\circ g) = \text{coe}(f) \circ \text{coe}(g)$$$

Lean4

@[simp, norm_cast]
theorem coe_comp (f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B) [MonoidHom.CompTriple φ ψ χ] : ⇑(f.comp g) = (⇑f) ∘ (⇑g) :=
  rfl

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

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

Разделы

Аффилиация

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