comp_sumAddHom — Mathlib

English

The composition of g with liftAddHom equals liftAddHom after composing g with each coordinate map.

Русский

Композиция g с liftAddHom равна liftAddHom от композиции g с каждой координатой.

LaTeX

$$$ g \\circ \\operatorname{liftAddHom} f = \\operatorname{liftAddHom} (a \\mapsto g \\circ (f a)). $$$

Lean4

theorem comp_sumAddHom {δ : Type*} [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] [AddCommMonoid δ] (g : γ →+ δ)
    (f : ∀ i, β i →+ γ) : g.comp (sumAddHom f) = sumAddHom fun a => g.comp (f a) :=
  comp_liftAddHom _ _

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