comul_assoc — Mathlib

English

Coassociativity of comultiplication: Δ ≫ t ◁ Δ = Δ ≫ Δ ▷ t ≫ (α_ t t t).hom.

Русский

Коассоциативность комулатирования: Δ ≫ t ◁ Δ = Δ ≫ Δ ▷ t ≫ (α_{t,t,t}).hom.

LaTeX

$$$Δ \\;≫\\; t \\triangleleft Δ = Δ \\;≫\\; Δ \\triangleright t \\;≫\\; (α_{t,t,t}).hom$$$

Lean4

@[reassoc (attr := simp)]
theorem comul_assoc : Δ ≫ t ◁ Δ = Δ ≫ Δ ▷ t ≫ (α_ t t t).hom :=
  ComonObj.comul_assoc t

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