∀ {G : Type u_2} {H : Type u_1} [inst : GroupWithZero G] [inst_1 : CommGroupWithZero H] (f : G →*₀ H) (n : ℕ)
  (a : ↥(MonoidHom.mrange f)), GroupWithZero.zpow (↑n.succ) a = GroupWithZero.zpow (↑n) a * a