no goals
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulLeft R a) ↔ IsNilpotent a
constructor <;> rintro ⟨n, hn⟩ <;> use n <;>
    simp only [mulLeft_eq_zero_iff, pow_mulLeft] at hn⊢ <;>
  exact hn