∀ {K : Type u} [inst : Field K] (p q : Polynomial K),
  ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).num =
    Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)