linearEquivFunOnFinite_single — Mathlib

English

For DecidableEq α, and x ∈ α, m ∈ M, the linear equivalence maps the finitely supported function that is 1 at x to the Dirac function at x.

Русский

Пусть α конечно; для x ∈ α, m ∈ M линейное эквивалентное отображение переводит единичную функцию в диракову функцию в x.

LaTeX

$$$(linearEquivFunOnFinite R M α)(\\text{single } x m) = \\Pi\\text{-single } x m$.$$

Lean4

@[simp]
theorem linearEquivFunOnFinite_single [DecidableEq α] (x : α) (m : M) :
    (linearEquivFunOnFinite R M α) (single x m) = Pi.single x m :=
  equivFunOnFinite_single x m

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