of_comul — Mathlib

English

The comultiplication on the lifted Hopf algebra matches the comultiplication on the original X; comul(A := of R X) = comul(R X).

Русский

Копмультипликaция поднятой Hopf-алгебры совпадает с комультипликацией исходного X; comul(A := of R X) = comul(R X).

LaTeX

$$$\mathrm{Coalgebra.comul}(A := \mathrm{of} \, R X) = \mathrm{Coalgebra.comul}(R := R)(A := X)$$$

Lean4

@[simp]
theorem of_comul {X : Type v} [Ring X] [HopfAlgebra R X] :
    Coalgebra.comul (A := of R X) = Coalgebra.comul (R := R) (A := X) :=
  rfl

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