∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (B : Type u_2) [inst_1 : CommSemiring B] [inst_2 : Algebra R B]
  [inst_3 : IsLocalization.Away x B] {n : ℤ}, 0 ≤ n → selfZPow x B n = (algebraMap R B) x ^ n.natAbs