of_comul — Mathlib

English

Equality of comultiplications under the of-construction: coalgebra comultiplication on of(R,X) equals that on X.

Русский

Суммарное повторение: комумуляция через of(R,X) равна коммуляции X.

LaTeX

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

Lean4

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

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