isNilpotent_mul_left_iff — Mathlib

English

Let R be a semiring and x, y ∈ R with x and y commuting, and suppose x is a left non-zero-divisor. Then x·y is nilpotent if and only if y is nilpotent.

Русский

Пусть R — полугруппа с нулём, x и y коммутируют, и x является левым ненулевым делителем. Тогда x·y нилпотентно тогда и только тогда, когда y нилпотентен.

LaTeX

$$$ (Commute\\ x\\ y) \\land (x \\in \\mathrm{nonZeroDivisorsLeft}\\ R) \\Rightarrow \\bigl( \\IsNilpotent(xy) \\iff \\IsNilpotent(y) \\bigr) $$$

Lean4

protected theorem isNilpotent_mul_left_iff (h_comm : Commute x y) (hx : x ∈ nonZeroDivisorsLeft R) :
    IsNilpotent (x * y) ↔ IsNilpotent y :=
  by
  refine ⟨?_, h_comm.isNilpotent_mul_left⟩
  rintro ⟨k, hk⟩
  rw [mul_pow h_comm] at hk
  exact ⟨k, (nonZeroDivisorsLeft R).pow_mem hx k _ hk⟩

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