comul_C_mul_T

Mathlib.RingTheory.Coalgebra.MonoidAlgebra

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

← MathLib Explorer

English

LaurentPolynomial is cocommutative when A is cocommutative.

Русский

LaurentPolynomial ко-коммутативна, когда A ко-коммутативна.

LaTeX

$$$\text{IsCocomm}\; R\; A[\mathbb{Z}]$$$

Lean4

@[simp]
theorem comul_C_mul_T (a : A) (n : ℤ) :
    Coalgebra.comul (R := R) (C a * T n) = TensorProduct.map (lsingle n) (lsingle n) (Coalgebra.comul (R := R) a) := by
  simp [← single_eq_C_mul_T]

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

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

Разделы

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

Аффилиация

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