English
There is an additive equivalence between finsupp on a dependent sum and a family of finsupps, given by the same underlying map with pointwise addition.
Русский
Существуют аддитивные эквивалентности между финспп на зависимой сумме и семейством финспп, задаваемые той же связью с поэлементным сложением.
LaTeX
$$$\\sigmaFinsuppAddEquivPiFinsupp : ((\\\\Sigma j, ιs j) \\\\to_0 α) \\\\simeq_+ ∀ j, ιs j \\\\to_0 α$$$
Lean4
/-- On a `Fintype η`, `Finsupp.split` is an additive equivalence between
`(Σ (j : η), ιs j) →₀ α` and `Π j, (ιs j →₀ α)`.
This is the `AddEquiv` version of `Finsupp.sigmaFinsuppEquivPiFinsupp`.
-/
noncomputable def sigmaFinsuppAddEquivPiFinsupp {α : Type*} {ιs : η → Type*} [AddMonoid α] :
((Σ j, ιs j) →₀ α) ≃+ ∀ j, ιs j →₀ α :=
{ sigmaFinsuppEquivPiFinsupp with
map_add' := fun f g => by
ext
simp }
