antipode_T

Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra

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

← MathLib Explorer

English

In LaurentPolynomial, antipode of T^n is T^{-n}.

Русский

В LaurentPolynomial антипод T^n равен T^{-n}.

LaTeX

$$$\text{antipode}\,R\,(T^n) = T^{-n}$$$

Lean4

@[simp]
theorem antipode_T (n : ℤ) : HopfAlgebra.antipode R (T n : A[T;T⁻¹]) = T (-n) :=
  by
  unfold T
  rw [AddMonoidAlgebra.antipode_single]
  simp only [HopfAlgebra.antipode_one, single_eq_C_mul_T, map_one, one_mul]

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

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

Разделы

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

Аффилиация

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