no goals
K : Type u
inst✝ : Field K
x : RatFunc K
⊢ Monic (denom x)
induction x using RatFunc.induction_on with
  | f p q hq =>
    rw [denom_div p hq, mul_comm]
    exact Polynomial.monic_mul_leadingCoeff_inv (right_div_gcd_ne_zero hq)
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ Monic (q / gcd p q * ↑C (leadingCoeff (q / gcd p q))⁻¹)
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ Monic (denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q))
rw [denom_div p hq, mul_comm]
no goals
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ Monic (q / gcd p q * ↑C (leadingCoeff (q / gcd p q))⁻¹)
exact Polynomial.monic_mul_leadingCoeff_inv (right_div_gcd_ne_zero hq)