comul_tmul — Mathlib

English

If A and B are cocommutative coalgebras over S and R respectively, then A ⊗_R B is cocommutative over S; i.e., the commutator of comul on the tensor product is symmetric.

Русский

Если A и B — копоммутативные коалгебры над S и R соответственно, то A ⊗_R B — копоммутативная над S; то есть копуляция на тензорном произведении симметрична.

LaTeX

$$$\text{IsCocomm}_S(A) \wedge \text{IsCocomm}_R(B) \Rightarrow \text{IsCocomm}_S(A \otimes_R B).$$$

Lean4

@[simp]
theorem comul_tmul (x : A) (y : B) :
    comul (x ⊗ₜ y) = AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B (comul x ⊗ₜ comul y) :=
  rfl

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