lsingle — Mathlib

English

For each index i, the linear map lsingle i: M_i → DFinsupp ι M_i sends x to the elementary dfinsupp with support at i equal to x.

Русский

Для каждого индекса i линейное отображение lsingle i: M_i → DFinsupp ι M_i отправляет x в элементарный dfinsupp, опора которого в точке i равна x.

LaTeX

$$$\\mathrm{lsingle}(i)\\colon M_i \\to_ℓ[R] \\Pi_0 i, M_i\\quad\\text{так что}\\quad (\\mathrm{lsingle}(i))(x) = \\delta_i(x)$$$

Lean4

/-- `DFinsupp.single` as a `LinearMap` -/
def lsingle (i) : M i →ₗ[R] Π₀ i, M i :=
  { DFinsupp.singleAddHom _ _ with
    toFun := single i
    map_smul' := single_smul }

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