counit_comp_lsingle

Mathlib.RingTheory.Coalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Finsupp.counit_comp_lsingle

English

The counit composed with lsingle_i equals the counit on A.

Русский

Коунит, композиция с lsingle_i, равен коуниту A.

LaTeX

$$$ \operatorname{counit} \circ \mathrm{lsingle}_{i} = \operatorname{counit} $$$

Lean4

@[simp]
theorem counit_comp_lsingle (i : ι) : counit ∘ₗ (lsingle i : A →ₗ[R] _) = counit := by ext; simp

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

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

Разделы

Аффилиация

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