map_comp — Mathlib

English

The map of a composition of component maps equals the composition of component maps after applying DirectSum.map.

Русский

Гомоморфизм DirectSum отображает композицию компонентных отображений как композицию соответствующих DirectSum.map.

LaTeX

$$$$\\mathrm{DirectSum.map}\\, (i \\mapsto (g_i \\circ f_i)) = (\\mathrm{DirectSum.map}\\, g) \\circ (\\mathrm{DirectSum.map}\\, f).$$$$

Lean4

@[simp]
theorem map_comp {γ : ι → Type*} [∀ i, AddCommMonoid (γ i)] (g : ∀ (i : ι), β i →+ γ i) :
    (map (fun i ↦ (g i).comp (f i))) = (map g).comp (map f) :=
  DFinsupp.mapRange.addMonoidHom_comp _ _

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