English
Let R be a semiring and x, y ∈ R with x and y commuting, and suppose y is a right non‑zero-divisor. Then x·y is nilpotent if and only if x is nilpotent.
Русский
Пусть R—полугруппа с нулём, причём элементы x, y коммутируют и y является правым НЗД (не нулевым делителем справа). Тогда x·y нилпотентно тогда и только тогда, когда x нилпотентен.
LaTeX
$$$ (Commute\\ x\\ y) \\land (y \\in \\mathrm{nonZeroDivisorsRight}\\ R) \\Rightarrow \\bigl( \\IsNilpotent(xy) \\iff \\IsNilpotent(x) \\bigr) $$$
Lean4
protected theorem isNilpotent_mul_right_iff (h_comm : Commute x y) (hy : y ∈ nonZeroDivisorsRight R) :
IsNilpotent (x * y) ↔ IsNilpotent x :=
by
refine ⟨?_, h_comm.isNilpotent_mul_right⟩
rintro ⟨k, hk⟩
rw [mul_pow h_comm] at hk
exact ⟨k, (nonZeroDivisorsRight R).pow_mem hy k _ hk⟩
