exists_eq_tmul_of_forall — Mathlib

English

The pure tensors span the entire tensor product; the submodule generated by all m ⊗ n is the whole space.

Русский

Чистые тензоры порождают всё тензорное произведение; подмодуль, порожденный всех m ⊗ n, равен всему пространству.

LaTeX

$$$\\operatorname{span}_R\\{ t : M \\otimes_R N \\mid \\exists m,n, m ⊗_R n = t\\} = \\top.$$$

Lean4

theorem exists_eq_tmul_of_forall (x : TensorProduct R M N)
    (h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ n₁ + m₂ ⊗ₜ n₂ = m ⊗ₜ[R] n) : ∃ m n, x = m ⊗ₜ n := by
  induction x with
  | zero =>
    use 0, 0
    rw [TensorProduct.zero_tmul]
  | tmul m n => use m, n
  | add x y h₁ h₂ =>
    obtain ⟨m₁, n₁, rfl⟩ := h₁
    obtain ⟨m₂, n₂, rfl⟩ := h₂
    apply h

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