∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} [inst_2 : Field L] (φ : Polynomial K →+* L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p q : Polynomial K),
  (RatFunc.liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) /
      (RatFunc.liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) q) =
    φ p / φ q