finsuppScalarRight — Mathlib

English

For m ∈ M, p ∈ Finsupp ι R, i ∈ ι, the i-th value of finsuppScalarRight(m ⊗ p) is p(i)·m.

Русский

Для m ∈ M, p ∈ Finsupp ι R, i ∈ ι, значение i в finsuppScalarRight(m ⊗ p) равно p(i)·m.

LaTeX

$$$ finsuppScalarRight R M ι (m \\otimes p) i = p(i) \\cdot m $$$

Lean4

/-- The tensor product of `M` and `ι →₀ R` is linearly equivalent to `ι →₀ M` -/
noncomputable def finsuppScalarRight : M ⊗[R] (ι →₀ R) ≃ₗ[R] ι →₀ M :=
  finsuppRight R M R ι ≪≫ₗ Finsupp.mapRange.linearEquiv (TensorProduct.rid R M)

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