linearEquivFunOnFinite — Mathlib

English

If α is finite, the natural linear isomorphism between finitely supported functions α →₀ M and all functions α → M is an R-linear equivalence.

Русский

Если α конечен, естественная линейная взаимно однозначность между функциями с конечной поддержкой α →₀ M и всеми функциями α → M является R-симметрической эквивалентностью.

LaTeX

$$$(\\alpha \\to_0 M) \\cong_R (\\alpha \\to M)$, при конечности α.$$

Lean4

/-- Given `Finite α`, `linearEquivFunOnFinite R` is the natural `R`-linear equivalence between
`α →₀ β` and `α → β`. -/
@[simps apply]
noncomputable def linearEquivFunOnFinite : (α →₀ M) ≃ₗ[R] α → M :=
  { equivFunOnFinite with
    toFun := (⇑)
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl }

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