∀ {A : Type u_3} {B : Type u_2} {α : Type u_1} [inst : Zero α] [inst_1 : AddMonoid A] [inst_2 : SMul α A]
  [inst_3 : SMul α B] [DivisibleBy A α] (f : A → B),
  Function.Surjective f → (∀ (a : A) (n : α), f (n • a) = n • f a) → ∀ {n : α}, n ≠ 0 → ∀ (x : B), ∃ a, n • a = x