eq_repr_basis_right — Mathlib

English

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

Русский

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

LaTeX

$$∃ b : κ →₀ M, Eq (b.sum (fun i m ⇒ m ⊗ 𝒞 i)) x$$

Lean4

/-- Elements in `M ⊗ N` can be represented by sum of elements in `M` tensor elements of basis of
`N`. -/
theorem eq_repr_basis_right : ∃ b : κ →₀ M, b.sum (fun i m ↦ m ⊗ₜ 𝒞 i) = x := by
  classical simpa using (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.surjective x

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