∀ {K : Type u_2} {L : Type u_1} [inst : Zero K] [inst_1 : Add K] [inst_2 : One K] [inst_3 : Mul K] [inst_4 : SMul ℕ K]
  [inst_5 : SMul ℚ≥0 K] [inst_6 : Pow K ℕ] [inst_7 : NatCast K] [inst_8 : NNRatCast K] (f : K → L)
  (hf : Function.Injective f) [inst_9 : DivisionSemiring L] (zero : f 0 = 0) (one : f 1 = 1)
  (add : ∀ (x y : K), f (x + y) = f x + f y) (mul : ∀ (x y : K), f (x * y) = f x * f y)
  (nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x),
  (∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x) →
    ∀ (npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ℕ), f ↑n = ↑n),
      (∀ (q : ℚ≥0), f ↑q = ↑q) → ∀ (q : ℚ≥0) (a : K), f (q • a) = f (↑q * a)