From 4435e909d7394707e958143ca914544c1cd9ee0c Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Sat, 4 Sep 2021 11:21:20 +0000
Subject: [PATCH] feat(ring_theory/ideal/operations): ideal.pow_mem_pow (#8996)

---
 src/ring_theory/ideal/operations.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/ring_theory/ideal/operations.lean b/src/ring_theory/ideal/operations.lean
index 032ae0216dd73..5d45eb262ed36 100644
--- a/src/ring_theory/ideal/operations.lean
+++ b/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