counitCoalgHom_apply

Mathlib.RingTheory.Coalgebra.Hom

URI: https://scilib.ai/kg/mathlib#Coalgebra.counitCoalgHom_apply

English

For x ∈ A, counitCoalgHom_R_A x equals counit x.

Русский

Для x ∈ A, counitCoalgHom_R_A x равно counit x.

LaTeX

$$$\mathrm{counitCoalgHom}\,R\,A\,x = \mathrm{counit}\,x$$$

Lean4

@[simp]
theorem counitCoalgHom_apply (x : A) : counitCoalgHom R A x = counit x :=
  rfl

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

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

Разделы

Аффилиация

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