span_tprod_eq_top — Mathlib

English

The pure tensors span the tensor product: Submodule.span R (Set.range (tprod R)) = ⊤.

Русский

Чистые тензоры образуют порождающее множество тензорного произведения: Span_R(Set.range(tprod R)) = ⊤.

LaTeX

$$$$ \operatorname{span}_R(\operatorname{range}(tprod R)) = (\top)$$$$

Lean4

/-- The pure tensors (i.e. the elements of the image of `PiTensorProduct.tprod`) span
the tensor product. -/
theorem span_tprod_eq_top : Submodule.span R (Set.range (tprod R)) = (⊤ : Submodule R (⨂[R] i, s i)) :=
  Submodule.eq_top_iff'.mpr fun t ↦
    t.induction_on
      (fun _ _ ↦ Submodule.smul_mem _ _ (Submodule.subset_span (by simp only [Set.mem_range, exists_apply_eq_apply])))
      (fun _ _ hx hy ↦ Submodule.add_mem _ hx hy)

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