feat(ring_theory/ideal/operations): ideal.pow_mem_pow (#8996)

src/ring_theory/ideal/operations.lean

@@ -273,6 +273,12 @@ submodule.smul_mem_smul hr hs
 theorem mul_mem_mul_rev {r s} (hr : r ∈ I) (hs : s ∈ J) : s * r ∈ I * J :=
 mul_comm r s ▸ mul_mem_mul hr hs
 
+lemma pow_mem_pow {x : R} (hx : x ∈ I) (n : ℕ) : x ^ n ∈ I ^ n :=
+begin
+  induction n with n ih, { simp only [pow_zero, ideal.one_eq_top], },
+  simpa only [pow_succ] using mul_mem_mul hx ih,
+end
+
 theorem mul_le : I * J ≤ K ↔ ∀ (r ∈ I) (s ∈ J), r * s ∈ K :=
 submodule.smul_le