finsuppUnique_apply — Mathlib

English

For ι Unique, the image of finsuppUnique by AddEquiv equals Equiv.finsuppUnique; i.e., the two representations coincide as functions.

Русский

Для уникального множества индексов выполняется совпадение двух стандартных отображений над finsupp.

LaTeX

$$$AddEquiv.finsuppUnique v = Equiv.finsuppUnique v$$$

Lean4

@[simp]
theorem _root_.AddEquiv.finsuppUnique_apply {ι : Type*} [Unique ι] (v : ι →₀ M) :
    AddEquiv.finsuppUnique v = Equiv.finsuppUnique v :=
  rfl

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