antipode_C

Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra

URI: https://scilib.ai/kg/mathlib#LaurentPolynomial.antipode_C

← MathLib Explorer

English

In LaurentPolynomial, antipode applied to C(a) equals C(antipode(a)).

Русский

В LaurentPolynomial антипод на C(a) даёт C(антпода(a)).

LaTeX

$$@[simp] theorem antipode_C (a : A) : HopfAlgebra.antipode R (C a) = C (HopfAlgebra.antipode R a) :=$$

Lean4

@[simp]
theorem antipode_C (a : A) : HopfAlgebra.antipode R (C a) = C (HopfAlgebra.antipode R a) :=
  by
  rw [← single_eq_C, AddMonoidAlgebra.antipode_single]
  simp

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

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

Разделы

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

Аффилиация

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