id_comp

Mathlib.RingTheory.Coalgebra.Hom

URI: https://scilib.ai/kg/mathlib#CoalgHom.id_comp

English

For φ: A →ₗc[R] B, composing on the left with the identity on B yields φ: (CoalgHom.id R B).comp φ = φ.

Русский

Для φ: A →ₗc[R] B композиция слева с тождественным отображением на B дает φ: (CoalgHom.id R B).comp φ = φ.

LaTeX

$$$(\mathrm{id}_B) \circ \varphi = \varphi$$$

Lean4

@[simp]
theorem id_comp : (CoalgHom.id R B).comp φ = φ :=
  ext fun _x => rfl

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

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

Разделы

Аффилиация

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