sigmaFinsuppEquivDFinsupp_apply — Mathlib

English

For any f : Π₀ i, η i →₀ N, and s : Σ i, η i, the symm image computes to f s.1 s.2.

Русский

Для любого f: Π₀ i, η i →₀ N и элемента s: Σ i, η i, симметричное отображение даёт f s.1 s.2.

LaTeX

$$$(\\sigmaFinsuppEquivDFinsupp.symm f) s = f\,s.1\,s.2$$$

Lean4

@[simp]
theorem sigmaFinsuppEquivDFinsupp_apply [Zero N] (f : (Σ i, η i) →₀ N) :
    (sigmaFinsuppEquivDFinsupp f : ∀ i, η i →₀ N) = Finsupp.split f :=
  rfl

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