comul_C_mul_T_self — Mathlib

English

In Laurent polynomial coalgebra, comultiplication distributes across the C and T generators in a simple product form: comul (C(a) · T^n) = T^n ⊗ (C(a) · T^n).

Русский

В коалгебре Лаурента комул распределяется по генераторам C и T в простом виде: comul( C(a) · T^n ) = T^n ⊗ ( C(a) · T^n ).

LaTeX

$$$\\mathrm{Coalgebra}.\\mathrm{comul}( C(a) \\cdot T^n ) = T^n \\otimes ( C(a) \\cdot T^n )$$$

Lean4

theorem comul_C_mul_T_self (a : R) (n : ℤ) : Coalgebra.comul (C a * T n) = T n ⊗ₜ[R] (C a * T n) := by simp

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