finsuppUnique_symm — Mathlib

English

The inverse of the canonical finsupp unique equivalence at d is the singleton at the unit: AddEquiv.finsuppUnique.symm d = single () d.

Русский

Обратное к каноническому едваёжному соответствию finsuppUnique равно одиночной функции на единице: AddEquiv.finsuppUnique.symm d = single () d.

LaTeX

$$$AddEquiv.finsuppUnique.symm\\; d = \\mathrm{single}\\;()\\;d$$$

Lean4

theorem _root_.AddEquiv.finsuppUnique_symm {M : Type*} [AddZeroClass M] (d : M) :
    AddEquiv.finsuppUnique.symm d = single () d :=
  by
  rw [Finsupp.unique_single (AddEquiv.finsuppUnique.symm d), Finsupp.unique_single_eq_iff]
  simp [AddEquiv.finsuppUnique]

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