Theorem: DividedPowers.dpow_eval_zero (DividedPowers/Basic.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 = 0
Tactic:
rw [← MulZeroClass.mul_zero (0 : A), hI.dpow_smul n I.zero_mem,
  zero_pow hn, zero_mul, zero_mul]
State after:
no goals