Is Nilpotent if a power is Nilpotent

Stream: Is there code for X?

[Xavier Xarles]

I don't find in mathlib4

import Mathlib.RingTheory.Nilpotent

variable {R : Type*}

theorem  IsNilpotent.if_pow [MonoidWithZero R] (x : R)(m:ℕ)(h:IsNilpotent (x ^ m)): IsNilpotent x := by
  obtain ⟨n, h⟩ := h
  use (m*n)
  rw [← h, pow_mul x m n]

[Ruben Van de Velde]

I think you're right. Want to make a PR? Call it of_pow, though

[Ruben Van de Velde]

And the iff version assuming n ne 0

[Jireh Loreaux]

And while you're at it maybe you can rename docs#IsNilpotent.pow to IsNilpotent.pow_succ and make the argument n explicit.