Theorem: DividedPowers.RatAlgebra.dpow_eq_of_mem (DividedPowers/RatAlgebra.lean)

State before:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
n : ℕ
x : R
hx : x ∈ I
⊢ dpow I n x = Ring.inverse ↑n ! * x ^ n
Tactic:
rw [dpow, OfInvertibleFactorial.dpow_eq_of_mem _ hx]
State after:
no goals