Theorem: DividedPowers.OfInvertibleFactorial.dpow_mem (DividedPowers/RatAlgebra.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I
⊢ dpow I m x ∈ I
Tactic:
rw [dpow_eq_of_mem m hx]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I
⊢ Ring.inverse ↑m ! * x ^ m ∈ I

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I
⊢ Ring.inverse ↑m ! * x ^ m ∈ I
Tactic:
exact Ideal.mul_mem_left I _ (Ideal.pow_mem_of_mem I hx _ (Nat.pos_of_ne_zero hm))
State after:
no goals