English
There is a canonical linear equivalence between finsupp on a sum type and the product of finsupps on each component.
Русский
Существует каноническое линейное эквивалентное отображение между Finsupp на сумме типов и произведением Finsupp на каждую компоненту.
LaTeX
$$$ (\alpha \oplus \beta) \to_0 M \cong_R (\alpha \to_0 M) \times (\beta \to_0 M) $$$
Lean4
/-- The linear equivalence between `(α ⊕ β) →₀ M` and `(α →₀ M) × (β →₀ M)`.
This is the `LinearEquiv` version of `Finsupp.sumFinsuppEquivProdFinsupp`. -/
@[simps apply symm_apply]
def sumFinsuppLEquivProdFinsupp {α β : Type*} : (α ⊕ β →₀ M) ≃ₗ[R] (α →₀ M) × (β →₀ M) :=
{ sumFinsuppAddEquivProdFinsupp with
map_smul' := by
intros
ext <;>
simp only [AddEquiv.toFun_eq_coe, Prod.smul_fst, Prod.smul_snd, smul_apply, snd_sumFinsuppAddEquivProdFinsupp,
fst_sumFinsuppAddEquivProdFinsupp, RingHom.id_apply] }
