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

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
x : A
hx : x ∈ I
⊢ dpow I 1 x = x
Tactic:
rw [dpow_eq_of_mem 1 hx, pow_one, Nat.factorial_one, Nat.cast_one, Ring.inverse_one, one_mul]
State after:
no goals