counit_single

Mathlib.RingTheory.Coalgebra.Basic

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

English

For any index i and element a, counit of Finsupp.single i a equals counit of a in A.

Русский

Для любого индекса i и элемента a, коунит Finsupp.single i a равен коуниту a.

LaTeX

$$$\operatorname{counit}(\mathrm{Finsupp}.\mathrm{single}_{i} a) = \operatorname{counit}(a)$$$

Lean4

@[simp]
theorem counit_single (i : ι) (a : A) : counit (Finsupp.single i a) = counit (R := R) a :=
  lsum_single _ _ _ _

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

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

Разделы

Аффилиация

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