finsuppUnique_apply — Mathlib

English

The canonical linear equivalence sends a finitely supported function f to its value at the unique element of α.

Русский

Каноническое линейное эквивалентность отображает почти на значение функции в уникальном элементе α.

LaTeX

$$$\text{finsuppUnique }\_R\ M\ α\ f = f(\text{default})$$$

Lean4

@[simp]
theorem finsuppUnique_apply (f : α →₀ M) : LinearEquiv.finsuppUnique R M α f = f default :=
  rfl

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