sigmaFinsuppLEquivPiFinsupp_apply

English

For a pair (j,i), the symmetric image yields the corresponding value at that pair.

Русский

Для пары (j,i) симметричное отображение даёт значение на этой паре.

LaTeX

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

Lean4

@[simp]
theorem sigmaFinsuppLEquivPiFinsupp_apply {M : Type*} {ιs : η → Type*} [AddCommMonoid M] [Module R M]
    (f : (Σ j, ιs j) →₀ M) (j i) : sigmaFinsuppLEquivPiFinsupp R f j i = f ⟨j, i⟩ :=
  rfl

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