linearMap — Mathlib

English

The linear map mapRange with a linear map is compatible with applying the underlying function mapRange: it acts componentwise on coordinates.

Русский

Линейное отображение mapRange совместимо с применением базовой функции mapRange: действует по координатам компонентно.

LaTeX

$$$mapRange.linearMap f : (α \\to_0 M) \\to α \\to_0 N$ with $f: M \\to_? N$$$

Lean4

/-- `Finsupp.mapRange` as a `LinearMap`. -/
@[simps apply]
def linearMap (f : M →ₛₗ[σ₁₂] N) : (α →₀ M) →ₛₗ[σ₁₂] α →₀ N :=
  {
    mapRange.addMonoidHom
      f.toAddMonoidHom with
    toFun := (mapRange f f.map_zero : (α →₀ M) → α →₀ N)
    map_smul' := fun c v => mapRange_smul' c (σ₁₂ c) v (f.map_smulₛₗ c) }

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