∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {R : Type u_1} [inst_2 : Monoid R]
  [inst_3 : DistribMulAction R (Polynomial K)] [inst_4 : IsScalarTower R (Polynomial K) (Polynomial K)] (c : R)
  (p q : Polynomial K),
  (algebraMap (Polynomial K) (RatFunc K)) (c • p) / (algebraMap (Polynomial K) (RatFunc K)) q =
    c • ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q)