English
There is a linear equivalence between DFinsupp over a product index and a nested dfinsupp over i with inner indices α i.
Русский
Существует линейное эквивалентное отображение между DFinsupp над произведением индексов и вложенным DFinsupp над i с внутренними индексами α i.
LaTeX
$$$\\mathrm{sigmaCurryLEquiv} : (Π_0 (i : (x : ι) × α x), M_i.fst i.snd) \\simeq_ℓ (Π_0 i (α i), M_i j)$$$
Lean4
/-- `DFinsupp.equivCongrLeft` as a linear equivalence.
This is the `DFinsupp` version of `Finsupp.domLCongr`. -/
@[simps! apply]
def domLCongr (e : ι ≃ ι') : (Π₀ i, M i) ≃ₗ[R] (Π₀ i, M (e.symm i))
where
__ := DFinsupp.equivCongrLeft e
map_add' _ _ := by ext; rfl
map_smul' _ _ := by ext; rfl
