zeroHom_comp — Mathlib

English

Composition of zeroHoms is respected by mapRange: mapRange.zeroHom (f.comp f₂) equals (mapRange.zeroHom f).comp (mapRange.zeroHom f₂).

Русский

Композиция нулевых гомоморфизмов сохраняется через mapRange: mapRange.zeroHom (f.comp f₂) = (mapRange.zeroHom f) .comp (mapRange.zeroHom f₂).

LaTeX

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

Lean4

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

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