lsingle_apply — Mathlib

English

lsingle a b is the finitely supported function that is b at a and zero elsewhere; it forms the standard basis element of the Finsupp direct sum.

Русский

lsingle a b — функция с конечной опорой, равная b при a и нулю в остальных местах; образует стандартный базис прямой суммы Finsupp.

LaTeX

$$$(lsingle\,a) : M \\to α\\to_0 M \\quad\\text{ satisfies } (lsingle\,a)\\, b = \\mathrm{single}\,a\,b$$$

Lean4

@[simp]
theorem lsingle_apply (a : α) (b : M) : (lsingle a : M →ₗ[R] α →₀ M) b = single a b :=
  rfl

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