no goals
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
⊢ ↑(algebraMap K[X] (RatFunc K)) (c • p) / ↑(algebraMap K[X] (RatFunc K)) q =
    c • (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)
rw [← mk_eq_div, mk_smul, mk_eq_div]