linearEquivFunOnFintype — Mathlib

English

The evaluation of lmk on x recovers mk s x.

Русский

Оценка lmk на x восстанавливает mk s x.

LaTeX

$$$ (\\mathrm{lmk}\\,s)\\; x = \\mathrm{mk}\\, s\\; x $$$

Lean4

/-- `DFinsupp.equivFunOnFintype` as a linear equivalence.

This is the `DFinsupp` version of `Finsupp.linearEquivFunOnFintype`. -/
@[simps! apply symm_apply]
def linearEquivFunOnFintype [Fintype ι] : (Π₀ i, M i) ≃ₗ[R] (Π i, M i)
    where
  __ := equivFunOnFintype
  map_add' _ _ := by ext; rfl
  map_smul' _ _ := by ext; rfl

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