∀ {A : Type u_1} [inst : CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [inst_1 : CommRing B]
  (f : A →+* B) (n : ℕ),
  DividedPowers.Quotient.OfSurjective.dpow hI f n = Function.extend (fun a => f ↑a) (fun a => f (hI.dpow n ↑a)) 0