comp

Mathlib.Algebra.Group.Hom.CompTypeclasses

URI: https://scilib.ai/kg/mathlib#MonoidHom.CompTriple.comp

← MathLib Explorer

English

φ, ψ and ψ ∘ φ form a CompTriple.

Русский

φ, ψ и ψ ∘ φ образуют CompTriple.

LaTeX

$$$$ \text{CompTriple }(\varphi, \psi, \psi \circ \varphi). $$$$

Lean4

/-- `φ`, `ψ` and `ψ.comp φ` form a `MonoidHom.CompTriple`

  (to be used with care, because no simplification is done) -/
theorem comp {φ : M →* N} {ψ : N →* P} : CompTriple φ ψ (ψ.comp φ) where comp_eq := rfl

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

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

Разделы

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

Аффилиация

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