map_neg — Mathlib

English

Let f be a ring homomorphism and u a unit in α. Then f(-u) = -f(u).

Русский

Пусть f — кольцевой гомоморфизм и u — единица в α. Тогда f(-u) = -f(u).

LaTeX

$$$f(-u) = -f(u)$$$

Lean4

@[simp]
protected theorem map_neg {F : Type*} [Ring β] [FunLike F α β] [RingHomClass F α β] (f : F) (u : αˣ) :
    map (f : α →* β) (-u) = -map (f : α →* β) u :=
  ext (by simp only [coe_map, Units.val_neg, MonoidHom.coe_coe, map_neg])

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