feat : add lemma on nilpotent and powers (#8831)

Changed `IsNilpotent.pow to IsNilpotent.pow_succ`. Added `IsNilpotent.of_pow` and `IsNilpotent.pow_iff_pos`.



Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

Author: XavierXarles

Mathlib/RingTheory/Nilpotent.lean

@@ -58,17 +58,28 @@ theorem IsNilpotent.neg [Ring R] (h : IsNilpotent x) : IsNilpotent (-x) := by
   rw [neg_pow, hn, mul_zero]
 #align is_nilpotent.neg IsNilpotent.neg
 
-lemma IsNilpotent.pow {n : ℕ} {S : Type*} [MonoidWithZero S] {x : S}
+lemma IsNilpotent.pow_succ (n : ℕ) {S : Type*} [MonoidWithZero S] {x : S}
     (hx : IsNilpotent x) : IsNilpotent (x ^ n.succ) := by
   obtain ⟨N,hN⟩ := hx
   use N
   rw [← pow_mul, Nat.succ_mul, pow_add, hN, mul_zero]
 
+theorem  IsNilpotent.of_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]
+
 lemma IsNilpotent.pow_of_pos {n} {S : Type*} [MonoidWithZero S] {x : S}
     (hx : IsNilpotent x) (hn : n ≠ 0) : IsNilpotent (x ^ n) := by
   cases n with
   | zero => contradiction
-  | succ => exact IsNilpotent.pow hx
+  | succ => exact  IsNilpotent.pow_succ _ hx
+
+@[simp]
+lemma IsNilpotent.pow_iff_pos {n} {S : Type*} [MonoidWithZero S] {x : S}
+    (hn : n ≠ 0) : IsNilpotent (x ^ n) ↔ IsNilpotent x :=
+ ⟨fun h => of_pow h, fun h => pow_of_pos h hn⟩
 
 @[simp]
 theorem isNilpotent_neg_iff [Ring R] : IsNilpotent (-x) ↔ IsNilpotent x :=