of_counit

Mathlib.Algebra.Category.BialgCat.Basic

URI: https://scilib.ai/kg/mathlib#BialgCat.of_counit

English

The counit of the algebra obtained by of(R,X) equals the counit of X.

Русский

Кауниут алгебры via of(R,X) равен кауниут X.

LaTeX

$$$$ \Coalgebra.counit(A := \text{of}(R,X)) = \Coalgebra.counit(R := R)(A := X). $$$$

Lean4

@[simp]
theorem of_counit {X : Type v} [Ring X] [Bialgebra R X] :
    Coalgebra.counit (A := of R X) = Coalgebra.counit (R := R) (A := X) :=
  rfl

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

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

Разделы

Аффилиация

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