∀ {G₀ : Type u_2} {G₀' : Type u_1} [inst : CommGroupWithZero G₀] [inst_1 : Zero G₀'] [inst_2 : Mul G₀']
  [inst_3 : One G₀'] [inst_4 : Inv G₀'] [inst_5 : Div G₀'] [inst_6 : Pow G₀' ℕ] [inst_7 : Pow G₀' ℤ] (h01 : 0 ≠ 1)
  (f : G₀ → G₀') (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1)
  (mul : ∀ (x y : G₀), f (x * y) = f x * f y) (inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹)
  (div : ∀ (x y : G₀), f (x / y) = f x / f y) (npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n) (a : G₀'), 0 * a = 0