counit_T

Mathlib.RingTheory.Bialgebra.MonoidAlgebra

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

English

The counit of LaurentPolynomial T-n is the unit 1 of the base ring: counit_T n = 1 for all n ∈ ℤ.

Русский

Куниcт LaurentPolynomial T_n принимает значение 1 для всех целых n.

LaTeX

$$counit_T (n) : Coalgebra.counit (R := R) (T n : A[T;T^{-1}]) = 1$$

Lean4

@[simp]
theorem counit_T (n : ℤ) : Coalgebra.counit (R := R) (T n : A[T;T⁻¹]) = 1 := by simp [T, -single_eq_C_mul_T]

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

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

Разделы

Аффилиация

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