comul_comp_lsingle — Mathlib

English

For a fixed i, comul after lsingle_i equals TensorProduct.map(lsingle_i, lsingle_i) after comul on A_i.

Русский

Для фиксированного i копуляция после lsingle_i равна TensorProduct.map(lsingle_i, lsingle_i) после копуляции на A_i.

LaTeX

$$$ \operatorname{comul} \circ \mathrm{lsingle}_{i} = (\mathrm{TensorProduct.map} (\mathrm{lsingle}_{i}) (\mathrm{lsingle}_{i})) \circ \operatorname{comul}_{i} $$$

Lean4

theorem comul_comp_lsingle (i : ι) :
    comul ∘ₗ (lsingle i : A →ₗ[R] _) = TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul := by ext; simp

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