span_tprod_eq_top — Mathlib

English

The range of tprod is dense in the symmetric power; the pure tensors span the symmetric tensor power.

Русский

Область применения tprod порождает всю симметрическую тензорную часть; чистые тензоры образуют базис симметризированной степени.

LaTeX

$$$ Submodule.span(R\\, set.range (tprod R)) = \\top $$$

Lean4

/-- The pure tensors (i.e. the elements of the image of `SymmetricPower.tprod`) span the symmetric
tensor power. -/
theorem span_tprod_eq_top : Submodule.span R (Set.range (tprod R (ι := ι) (M := M))) = ⊤ := by
  rw [tprod, LinearMap.coe_compMultilinearMap, Set.range_comp, Submodule.span_image, PiTensorProduct.span_tprod_eq_top,
    Submodule.map_top, range_mk]

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