toDirectSum_ι — Mathlib

English

The image of ι under toDirectSum is the direct sum element corresponding to ι in degree 1.

Русский

Образ ι под действием toDirectSum соответствует элементу прямой суммы в степени 1.

LaTeX

$$$ toDirectSum (ι R x) = DirectSum.of (fun n => ⨂[R]^n M) _ (PiTensorProduct.tprod R fun _ : Fin 1 => x) $$$

Lean4

@[simp]
theorem toDirectSum_ι (x : M) :
    toDirectSum (ι R x) = DirectSum.of (fun n => ⨂[R]^n M) _ (PiTensorProduct.tprod R fun _ : Fin 1 => x) :=
  TensorAlgebra.lift_ι_apply _ _

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