sigmaFinsuppLEquivPiFinsupp — Mathlib

English

The symmetric version applied to a pair (j,i) gives the corresponding component value.

Русский

Обратное к паре (j,i) возвращает соответствующее значение компоненты.

LaTeX

$$((sumFinsuppLEquivProdFinsupp R).symm f) (j,i) = f j i$$

Lean4

/-- On a `Fintype η`, `Finsupp.split` is a linear equivalence between
`(Σ (j : η), ιs j) →₀ M` and `(j : η) → (ιs j →₀ M)`.

This is the `LinearEquiv` version of `Finsupp.sigmaFinsuppAddEquivPiFinsupp`. -/
noncomputable def sigmaFinsuppLEquivPiFinsupp {M : Type*} {ιs : η → Type*} [AddCommMonoid M] [Module R M] :
    ((Σ j, ιs j) →₀ M) ≃ₗ[R] (j : _) → (ιs j →₀ M) :=
  { sigmaFinsuppAddEquivPiFinsupp with
    map_smul' := fun c f => by
      ext
      simp }

Похожие утверждения