counit_algebraMap

Mathlib.RingTheory.Bialgebra.Basic

URI: https://scilib.ai/kg/mathlib#Bialgebra.counit_algebraMap

English

The counit composed with algebraMap R A is the identity on R: counit(algebraMap_R_A r) = r.

Русский

Коунил композиция с algebraMap R A даёт тождество на R: counit(algebraMap_R_A r) = r.

LaTeX

$$$\text{counit}(\text{algebraMap } R A\, r) = r$$$

Lean4

@[simp]
theorem counit_algebraMap (r : R) : counit (R := R) (algebraMap R A r) = r :=
  (counitAlgHom R A).commutes r

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

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

Разделы

Аффилиация

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