equivFinsuppOfBasisRight — Mathlib

English

Applying the right basis-equivariant map to m ⊗ n yields a linear combination where each coefficient is 𝒞.repr n i times m.

Русский

Применение правого отображения эквивалентности даёт линейную комбинацию, коэффициенты которой равны 𝒞.repr(n)i, умноженным на m.

LaTeX

$$$ (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m \otimes n) i = 𝒞.repr(n)(i) \cdot m $$$

Lean4

/-- If `{𝒞ᵢ}` is a basis for the module `N`, then every elements of `x ∈ M ⊗ N` can be uniquely written
as `∑ᵢ mᵢ ⊗ 𝒞ᵢ` for some `mᵢ ∈ M`.
-/
def equivFinsuppOfBasisRight : M ⊗[R] N ≃ₗ[R] κ →₀ M :=
  LinearEquiv.lTensor M 𝒞.repr ≪≫ₗ TensorProduct.finsuppScalarRight R M κ

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