lmap_comp — Mathlib

English

For any i, lmap f on lof_i(b) equals lof_i(f_i(b)).

Русский

Для любого i, lmap f на lof_i(b) даёт lof_i(f_i(b)).

LaTeX

$$$\\mathrm{lmap}\\ f\\ (\\mathrm{lof}\\,i\\ (b)) = \\mathrm{lof}\\,i\\ (f_i(b)).$$$

Lean4

@[simp]
theorem lmap_comp {K : ι → Type*} [∀ i, AddCommMonoid (K i)] [∀ i, Module R (K i)] (g : ∀ (i : ι), N i →ₗ[R] K i) :
    (lmap (fun i ↦ (g i) ∘ₗ (f i))) = (lmap g) ∘ₗ (lmap f) :=
  DFinsupp.mapRange.linearMap_comp _ _

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