finsuppUnique — Mathlib

English

If ι has a unique element, there is an equivalence between Finsupp ι M and M given by evaluation at the unique index.

Русский

Если у ι есть единственный элемент, существует эквивалентность между Finsupp ι M и M, задаваемая взятием значения в уникальном индексе.

LaTeX

$$Equiv (Finsupp ι M) M \\text{ for } [Unique ι]$$

Lean4

/-- If `α` has a unique term, the type of finitely supported functions `α →₀ β` is equivalent to `β`.
-/
@[simps!]
noncomputable def _root_.Equiv.finsuppUnique {ι : Type*} [Unique ι] : (ι →₀ M) ≃ M :=
  Finsupp.equivFunOnFinite.trans (Equiv.funUnique ι M)

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