isNilpotent_unit_mul_of_commute_iff

English

If u is a unit and r commutes with u in a monoid with zero, then IsNilpotent(r·u) ↔ IsNilpotent r.

Русский

Если u — единица, и r коммутирует с u в моноиде с нулём, то IsNilpotent(r·u) ⇔ IsNilpotent(r).

LaTeX

$$$ [MonoidWithZero\\ R] \\{r,u : R\\} (hu : \\IsUnit u) (h_comm : Commute r u) : \\IsNilpotent (r * u) \\iff \\IsNilpotent r $$$

Lean4

theorem isNilpotent_unit_mul_of_commute_iff [MonoidWithZero R] {r u : R} (hu : IsUnit u) (h_comm : Commute r u) :
    IsNilpotent (u * r) ↔ IsNilpotent r :=
  h_comm ▸ hu.isNilpotent_mul_unit_of_commute_iff h_comm

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