counit_comp_antipode

Mathlib.RingTheory.HopfAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#HopfAlgebra.counit_comp_antipode

English

The counit composed with antipode as a linear map equals the counit, i.e., counit ∘ antipode = counit.

Русский

Сопоставление counit и antipode как линейного отображения: counit ∘ antipode = counit.

LaTeX

$$$\text{counit} \circ_{\ell} \text{antipode } R = \text{counit}.$$$

Lean4

@[simp]
theorem counit_comp_antipode : counit ∘ₗ antipode R = counit (A := A) := by ext; exact counit_antipode _

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

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

Разделы

Аффилиация

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