comul_single — Mathlib

English

Comultiplication on a basis element in MonoidAlgebra: comul(single x a) = map (lsingle x) (lsingle x) (comul a).

Русский

Копупликация базисного элемента MonoidAlgebra: comul(single x a) = map (lsingle x) (lsingle x) (comul a).

LaTeX

$$$\mathrm{comul}(\mathrm{single}(x,a)) = \big(\mathrm{TensorProduct.map}(\mathrm{lsingle}(x), \mathrm{lsingle}(x))\big)(\mathrm{comul}(a))$$$

Lean4

@[simp]
theorem comul_single (x : X) (a : A) :
    Coalgebra.comul (R := R) (single x a) = TensorProduct.map (lsingle x) (lsingle x) (Coalgebra.comul a) :=
  Finsupp.comul_single _ _ _ _ _

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