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

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
x : A
hx : x ∈ I
⊢ dpow I 0 x = 1
Tactic:
simp only [dpow, factorial_zero, cast_one, Ring.inverse_one, _root_.pow_zero, mul_one, if_pos hx]
State after:
no goals