finsuppScalarLeft — Mathlib

English

There is a linear equivalence between (ι →₀ R) ⊗ N and ι →₀ N, turning a simple index coefficient into a simple tensor.

Русский

Существует линейное эквивалентное отображение между (ι →₀ R) ⊗ N и ι →₀ N, которое разворачивает коэффициент по индексу в простой тензор.

LaTeX

$$$ finsuppScalarLeft R N ι : (ι \\to_0 R) \\otimes_R N \\cong_ℓ R (ι \\to_0 N) $$$

Lean4

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

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