eq_repr_basis_left — Mathlib

English

There exists a representation of x in terms of left-basis coefficients.

Русский

Существует представление x через коэффициенты левого базиса.

LaTeX

$$∃ c : ι →₀ N, c.sum (fun i n ⇒ ℬ i ⊗ₜ n) = x$$

Lean4

/-- Elements in `M ⊗ N` can be represented by sum of elements of basis of `M` tensor elements of
  `N`. -/
theorem eq_repr_basis_left : ∃ (c : ι →₀ N), (c.sum fun i n ↦ ℬ i ⊗ₜ n) = x :=
  by
  classical obtain ⟨c, rfl⟩ := (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.surjective x
  exact ⟨c, (TensorProduct.comm R M N).injective <| by simp [Finsupp.sum]⟩

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