Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply (DividedPowers/SubDPIdeal.lean)

State before:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)
Tactic:
rw [dpow_def, dpow_apply' hI hIf ha]
State after:
no goals