K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ p / gcd p q ∣ p

K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ (leadingCoeff (q / gcd p q))⁻¹ ≠ 0
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ num (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) ∣ p
rw [num_div _ q, C_mul_dvd]
no goals
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ p / gcd p q ∣ p
exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_left p q)
no goals
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ (leadingCoeff (q / gcd p q))⁻¹ ≠ 0
simpa only [Ne.def, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero hq