map_zero — Mathlib

English

For any function f : α → β, applying the functor map to the zero element of FreeAbelianGroup α yields zero in FreeAbelianGroup β.

Русский

Для любой функции f : α → β применение отображения через отображение к нулю в FreeAbelianGroup α дает нуль в FreeAbelianGroup β.

LaTeX

$$$ \forall {\alpha \beta} (f : \alpha \to \beta),\; f <$> (0 : FreeAbelianGroup(\alpha)) = 0$$$

Lean4

@[simp]
protected theorem map_zero (f : α → β) : f <$> (0 : FreeAbelianGroup α) = 0 :=
  (lift (of ∘ f)).map_zero

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