isNilpotent_mulLeft_iff — Mathlib

English

For a module endomorphism linear map a ∈ A, Nilpotent(LinearMap.mulLeft R a) is equivalent to Nilpotent(a).

Русский

Для линейного отображения умножения слева нильпотентность эквивалентна нильпотентности элемента a.

LaTeX

$$IsNilpotent (LinearMap.mulLeft R a) ↔ IsNilpotent a$$

Lean4

@[simp]
theorem isNilpotent_mulLeft_iff (a : A) : IsNilpotent (mulLeft R a) ↔ IsNilpotent a := by
  constructor <;> rintro ⟨n, hn⟩ <;> use n <;> simp only [mulLeft_eq_zero_iff, pow_mulLeft] at hn ⊢ <;> exact hn

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