antipode_one

Mathlib.RingTheory.HopfAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#HopfAlgebra.antipode_one

← MathLib Explorer

English

In a Hopf algebra, the antipode sends the unit to the unit: antipode_R(1_A) = 1_A.

Русский

В гензелевой алгебре антипод отображает единицу в единицу: S(1) = 1.

LaTeX

$$$\mathrm{antipode}\,R\,(1_A) = 1_A.$$$

Lean4

@[simp]
theorem antipode_one : HopfAlgebra.antipode R (1 : A) = 1 := by
  simpa [Algebra.TensorProduct.one_def] using mul_antipode_rTensor_comul_apply (R := R) (1 : A)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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