case pos
K : Type u
inst✝ : Field K
p q : K[X]
hq : q = 0
⊢ denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) ∣ q

case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) ∣ q
K : Type u
inst✝ : Field K
p q : K[X]
⊢ denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) ∣ q
by_cases hq : q = 0
case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ q / gcd p q ∣ q

case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ (leadingCoeff (q / gcd p q))⁻¹ ≠ 0
case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) ∣ q
rw [denom_div _ hq, C_mul_dvd]
no goals
case pos
K : Type u
inst✝ : Field K
p q : K[X]
hq : q = 0
⊢ denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) ∣ q
simp [hq]
no goals
case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ q / gcd p q ∣ q
exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_right p q)
no goals
case neg
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