English
If every decomposition of a tensor into simple tensors can be matched to a single simple tensor, then the tensor is itself a simple tensor.
Русский
Если для каждого разложения тензора на простые тензоры можно подобрать одно простое тензорное произведение, то сам тензор распадается на один такой элемент.
LaTeX
$$$\\exists m\\in M,\\exists n\\in N,\\ x = m ⊗_R n,$ если для всех m_1,m_2,n_1,n_2\\,\\exists m,n,\\ m_1 ⊗_R n_1 + m_2 ⊗_R n_2 = m ⊗_R n.$$$
Lean4
/-- The simple (aka pure) elements span the tensor product. -/
theorem span_tmul_eq_top : Submodule.span R {t : M ⊗[R] N | ∃ m n, m ⊗ₜ n = t} = ⊤ :=
by
ext t; simp only [Submodule.mem_top, iff_true]
refine t.induction_on ?_ ?_ ?_
· exact Submodule.zero_mem _
· intro m n
apply Submodule.subset_span
use m, n
· intro t₁ t₂ ht₁ ht₂
exact Submodule.add_mem _ ht₁ ht₂
