∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] {I : Ideal A} [inst_1 : CommSemiring B] {J : Ideal B}
  {e : A ≃+* B} (h : Ideal.map e I = J) (hI : DividedPowers I) {n : ℕ} {b : B},
  (DividedPowers.ofRingEquiv h hI).dpow n b = e (hI.dpow n (e.symm b))