English
There is a natural linear equivalence between finitely supported functions on a product α × β with values in M and finitely supported functions from α to finitely supported functions β →₀ M.
Русский
Существует естественное линейное эквивалентное отображение между функциями с конечной поддержкой на произведении α × β, значения которых лежат в M, и функциями с конечной поддержкой от α в пространства β →₀ M.
LaTeX
$$$$ (α × β →_0 M) ≃_ℓ (α →_0 (β →_0 M)). $$$$
Lean4
/-- The linear equivalence between `α × β →₀ M` and `α →₀ β →₀ M`.
This is the `LinearEquiv` version of `Finsupp.finsuppProdEquiv`. -/
@[simps +simpRhs]
noncomputable def finsuppProdLEquiv : (α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M :=
{ finsuppProdEquiv with
map_add' f g := by ext; simp
map_smul' c f := by ext; simp }
