isNilpotent_mul_unit_of_commute_iff

English

Same injective-preserving/reflection property for nilpotency under monoid-with-zero homomorphisms.

Русский

Та же самая свойство сохранения/обращения нилпотентности под гомоморфизмами моноидов с нулём.

LaTeX

$$$ \\IsNilpotent(r) \\Rightarrow \\IsNilpotent(f(r)) \\text{ and } \\IsNilpotent(f(r)) \\Rightarrow \\IsNilpotent(r)$$$

Lean4

theorem isNilpotent_mul_unit_of_commute_iff [MonoidWithZero R] {r u : R} (hu : IsUnit u) (h_comm : Commute r u) :
    IsNilpotent (r * u) ↔ IsNilpotent r :=
  exists_congr fun n ↦ by rw [h_comm.mul_pow, (hu.pow n).mul_left_eq_zero]

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