case pos
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hpq : degree q ≤ degree p
hq : q = 0
⊢ leadingCoeff (p / q) = leadingCoeff p / leadingCoeff q

case neg
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hpq : degree q ≤ degree p
hq : ¬q = 0
⊢ leadingCoeff (p / q) = leadingCoeff p / leadingCoeff q
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hpq : degree q ≤ degree p
⊢ leadingCoeff (p / q) = leadingCoeff p / leadingCoeff q
by_cases hq : q = 0
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hpq : degree q ≤ degree p
hq : ¬q = 0
⊢ degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p
case neg
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hpq : degree q ≤ degree p
hq : ¬q = 0
⊢ leadingCoeff (p / q) = leadingCoeff p / leadingCoeff q
rw [div_def, leadingCoeff_mul, leadingCoeff_C,
  leadingCoeff_divByMonic_of_monic (monic_mul_leadingCoeff_inv hq) _, mul_comm,
  div_eq_mul_inv]
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hpq : degree q ≤ degree p
hq : ¬q = 0
⊢ degree (q * ↑C (leadingCoeff q)⁻¹) ≤ degree p
rwa [degree_mul_leadingCoeff_inv q hq]
no goals
case pos
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hpq : degree q ≤ degree p
hq : q = 0
⊢ leadingCoeff (p / q) = leadingCoeff p / leadingCoeff q
simp [hq]