addMonoidHom_comp — Mathlib

English

Composition of AddMonoidHom is preserved by mapRange: mapRange.addMonoidHom (f.comp f₂) equals (mapRange.addMonoidHom f).comp (mapRange.addMonoidHom f₂).

Русский

Композиция AddMonoidHom сохраняется через mapRange: mapRange.addMonoidHom (f.comp f₂) = (mapRange.addMonoidHom f).comp (mapRange.addMonoidHom f₂).

LaTeX

$$mapRange.addMonoidHom (f.comp f₂) = (mapRange.addMonoidHom f).comp (mapRange.addMonoidHom f₂)$$

Lean4

theorem addMonoidHom_comp (f : N →+ P) (f₂ : M →+ N) :
    (mapRange.addMonoidHom (f.comp f₂) : (α →₀ _) →+ _) = (mapRange.addMonoidHom f).comp (mapRange.addMonoidHom f₂) :=
  AddMonoidHom.ext <| mapRange_comp f (map_zero f) f₂ (map_zero f₂) (by simp only [comp_apply, map_zero])

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