instCoalgebra

Mathlib.RingTheory.Coalgebra.MonoidAlgebra

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

English

There is a coalgebra structure on LaurentPolynomial A, i.e., LaurentPolynomial R A[T;T⁻¹] is a coalgebra.

Русский

Существует коалгебраическая структура на LaurentPolynomial A: LaurentPolynomial R A[T;T⁻¹] — коалгебра.

LaTeX

$$$\text{Coalgebra}\; R\, A[T;T^{-1}]$$$

Lean4

instance instCoalgebra : Coalgebra R A[T;T⁻¹] :=
  inferInstanceAs <| Coalgebra R A[ℤ]

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

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

Разделы

Аффилиация

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