R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < degree q
hq0 : q ≠ 0
⊢ degree (p / q) < degree p
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < degree q
⊢ degree (p / q) < degree p
have hq0 : q ≠ 0 := fun hq0 => by simp [hq0] at hq
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < degree q
hq0 : q ≠ 0
⊢ degree (p /ₘ (q * ↑C (leadingCoeff q)⁻¹)) < degree p
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < degree q
hq0 : q ≠ 0
⊢ degree (p / q) < degree p
rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq0]
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]
hp : p ≠ 0
hq : 0 < degree q
hq0 : q ≠ 0
⊢ degree (p /ₘ (q * ↑C (leadingCoeff q)⁻¹)) < degree p
exact
  degree_divByMonic_lt _ (monic_mul_leadingCoeff_inv hq0) hp
    (by rw [degree_mul_leadingCoeff_inv _ hq0]; exact hq)
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]
hp : p ≠ 0
hq : 0 < degree q
hq0 : q = 0
⊢ False
simp [hq0] at hq
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < degree q
hq0 : q ≠ 0
⊢ 0 < degree q
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < degree q
hq0 : q ≠ 0
⊢ 0 < degree (q * ↑C (leadingCoeff q)⁻¹)
rw [degree_mul_leadingCoeff_inv _ hq0]
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]
hp : p ≠ 0
hq : 0 < degree q
hq0 : q ≠ 0
⊢ 0 < degree q
exact hq