finsuppUnique — Mathlib

English

If α has a unique term, then the finitely supported functions α →₀ M are linearly isomorphic to M via a natural evaluation map.

Русский

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

LaTeX

$$$(\alpha \to_0 M) \simeq_R M$$$

Lean4

/-- If `α` has a unique term, then the type of finitely supported functions `α →₀ M` is
`R`-linearly equivalent to `M`. -/
noncomputable def finsuppUnique : (α →₀ M) ≃ₗ[R] M :=
  {
    Finsupp.equivFunOnFinite.trans
      (Equiv.funUnique α M) with
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl }

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