antipode_eq_id

Mathlib.RingTheory.HopfAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#CommSemiring.antipode_eq_id

English

In the commutative setting, the antipode map is the identity on the underlying algebra; antipode R (A := R) = id.

Русский

В коммутативной ситуации antipode на кольце-основе равен тождественному отображению; antipode_R (A := R) = Id.

LaTeX

$$$\operatorname{antipode}\,R\,(A := R) = \mathrm{Id}.$$$

Lean4

@[simp]
theorem antipode_eq_id : antipode R (A := R) = .id :=
  rfl

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

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

Разделы

Аффилиация

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