sigmaFinsuppLequivDFinsupp — Mathlib

English

The function underlying finsuppLequivDFinsupp, when viewed on (ι →₀ M), is exactly Finsupp.toDFinsupp.

Русский

Функция, лежащая в основе finsuppLequivDFinsupp, на множестве (ι →₀ M) совпадает с Finsupp.toDFinsupp.

LaTeX

$$$\\bigl(\\text{toFunLike.coe}(\\text{finsuppLequivDFinsupp } R)\\bigr) F = Finsupp.toDFinsupp$$$

Lean4

/-- `Finsupp.split` is a linear equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. -/
@[simps]
def sigmaFinsuppLequivDFinsupp [AddCommMonoid N] [Module R N] : ((Σ i, η i) →₀ N) ≃ₗ[R] Π₀ i, η i →₀ N :=
  { sigmaFinsuppAddEquivDFinsupp with map_smul' := sigmaFinsuppEquivDFinsupp_smul }

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