counit_apply

Mathlib.RingTheory.Coalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Prod.counit_apply

English

For a product element (a,b), counit sums the counits of each coordinate.

Русский

Для элемента (a,b) коунит даёт сумму коунитов координат.

LaTeX

$$$(\\operatorname{counit}(a,b)) = \\operatorname{counit}(a) + \\operatorname{counit}(b).$$$

Lean4

@[simp]
theorem counit_apply (r : A × B) : (counit r : R) = counit r.1 + counit r.2 :=
  rfl

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

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

Разделы

Аффилиация

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