zeroHom_id — Mathlib

English

The zero mapRange on the identity zero map equals the identity zero map on the finsupp space.

Русский

Нулевая гомоморфная карта в пространстве конечносоподчиненных функций равна нулевой гомоморфной карте на пространстве FinSupp.

LaTeX

$$$mapRange.zeroHom(\\mathrm{ZeroHom.id}\\, M) = \\mathrm{ZeroHom.id}\\,(\\alpha \\to_0 M)$$$

Lean4

@[simp]
theorem zeroHom_id : mapRange.zeroHom (ZeroHom.id M) = ZeroHom.id (α →₀ M) :=
  ZeroHom.ext mapRange_id

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