English
Two linear maps F and G from DFinsupp to N coincide if they agree after summing over i with lsingle i.
Русский
Два линейных отображения F и G согласуются, если они дают одинаковый результат после суммирования по i через lsingle.
LaTeX
$$$\\mathrm{lsum}\\;F = \\mathrm{lsum}\\;G \\Rightarrow F = G$$$
Lean4
/-- `DFinsupp.sigmaCurryEquiv` as a linear equivalence.
This is the `DFinsupp` version of `Finsupp.finsuppProdLEquiv`. -/
@[simps! apply symm_apply]
def sigmaCurryLEquiv {α : ι → Type*} {M : (i : ι) → α i → Type*} [Π i j, AddCommMonoid (M i j)]
[Π i j, Module R (M i j)] [DecidableEq ι] :
(Π₀ (i : (x : ι) × α x), M i.fst i.snd) ≃ₗ[R] Π₀ (i : ι) (j : α i), M i j
where
__ := DFinsupp.sigmaCurryEquiv
map_add' _ _ := by ext; rfl
map_smul' _ _ := by ext; rfl
