comul_comp_inr — Mathlib

English

Comultiplication composed with the inr map equals the appropriate tensor map composed with comul.

Русский

Композиция копуляции с векторной вставкой inr равна соответствующему тензорному отображению, распространённому по copul.

LaTeX

$$$\\text{comul} \\circ \\mathrm{inr} = (\\mathrm{TensorProduct.map}(\\mathrm{inr},\\mathrm{inr})) \\circ \\mathrm{comul}$$$

Lean4

theorem comul_comp_inr : comul ∘ₗ inr R A B = TensorProduct.map (.inr R A B) (.inr R A B) ∘ₗ comul := by ext; simp

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