equivFinsuppOfBasisRight_symm — Mathlib

English

The map sending a coefficient function to the sum of its coefficients tensored with the basis elements on the right is injective.

Русский

Коэффициентная функция отображается в инъекцию через суммирование с тензоризацией по правому базису.

LaTeX

$$Function.Injective (Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N).flip (𝒞 i))$$

Lean4

theorem equivFinsuppOfBasisRight_symm :
    (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.toLinearMap =
      Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N).flip (𝒞 i) :=
  by ext; simp [equivFinsuppOfBasisRight]

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