equivFinsuppOfBasisLeft_apply_tmul_apply

English

Every element of M ⊗ N can be written as a finite sum of terms m_i ⊗ 𝒞_i with coefficients m_i in M.

Русский

Каждый элемент M ⊗ N можно записать как конечную сумму ∑ m_i ⊗ 𝒞_i с коэффициентами m_i из M.

LaTeX

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

Lean4

theorem equivFinsuppOfBasisLeft_apply_tmul_apply (m : M) (n : N) (i : ι) :
    (TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ n) i = ℬ.repr m i • n := by
  simp only [equivFinsuppOfBasisLeft_apply_tmul, Finsupp.mapRange_apply]

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