counit_single

Mathlib.RingTheory.Coalgebra.MonoidAlgebra

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

English

Counit on a basis element in AddMonoidAlgebra: counit(single x a) = counit a.

Русский

Коуниц на базисном элементе AddMonoidAlgebra: counit(single x a) = counit a.

LaTeX

$$$\mathrm{counit}(\mathrm{single}(x,a)) = \mathrm{counit}(a)$$$

Lean4

@[simp]
theorem counit_single (x : X) (a : A) : Coalgebra.counit (single x a) = Coalgebra.counit (R := R) a :=
  Finsupp.counit_single _ _ _ _ _

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

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

Разделы

Аффилиация

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