isNilpotent_mulRight_iff — Mathlib

English

Similarly, IsNilpotent (mulRight R a) ↔ IsNilpotent a.

Русский

Аналогично: нильпотентность от правого умножения равна нильпотентности элемента a.

LaTeX

$$IsNilpotent (mulRight R a) ↔ IsNilpotent a$$

Lean4

@[simp]
theorem isNilpotent_mulRight_iff (a : A) : IsNilpotent (mulRight R a) ↔ IsNilpotent a := by
  constructor <;> rintro ⟨n, hn⟩ <;> use n <;> simp only [mulRight_eq_zero_iff, pow_mulRight] at hn ⊢ <;> exact hn

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