equivFinsuppOfBasisLeft — Mathlib

English

The left-sum map from the basis to the tensor product is injective.

Русский

Левое суммирование по базису инъективно в тензорном произведении.

LaTeX

$$Function.Injective (Finsupp.lsum R fun i ⇢ (TensorProduct.mk R M N) (ℬ i))$$

Lean4

/-- If `{ℬᵢ}` is a basis for the module `M`, then every elements of `x ∈ M ⊗ N` can be uniquely written
as `∑ᵢ ℬᵢ ⊗ nᵢ` for some `nᵢ ∈ N`.
-/
def equivFinsuppOfBasisLeft : M ⊗[R] N ≃ₗ[R] ι →₀ N :=
  TensorProduct.comm R M N ≪≫ₗ TensorProduct.equivFinsuppOfBasisRight ℬ

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