lcoeFun — Mathlib

English

The forgetful map from finitely supported functions to ordinary functions is linear.

Русский

Отображение из Finsupp α M в α → M сохраняет линейность.

LaTeX

$$$\text{lcoeFun}: (α \to_0 M) \to_{R} (α \to M)$ является линейным отображением$$

Lean4

/-- Forget that a function is finitely supported.

This is the linear version of `Finsupp.toFun`. -/
@[simps]
def lcoeFun : (α →₀ M) →ₗ[R] α → M where
  toFun := (⇑)
  map_add' x
    y := by
    ext
    simp
  map_smul' x
    y := by
    ext
    simp

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