map — Mathlib

English

Nilpotent elements are preserved under monoid homomorphisms: if r is nilpotent in R, then f(r) is nilpotent in S for any monoid-with-zero homomorphism f.

Русский

Нилпотентность сохраняется под гомоморфизмами моноидов: если r нилпотентен в R, то f(r) нилпотентен в S для любого гомоморфизма f между моноидами с нулём.

LaTeX

$$$ \\IsNilpotent(r) \\Rightarrow \\IsNilpotent(f(r)) $$$

Lean4

theorem map [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type*} [FunLike F R S] [MonoidWithZeroHomClass F R S]
    (hr : IsNilpotent r) (f : F) : IsNilpotent (f r) :=
  by
  use hr.choose
  rw [← map_pow, hr.choose_spec, map_zero]

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