no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p✝ q✝ p q : R[X]
hq : q = 0
⊢ degree (p / q) ≤ degree p
simp [hq]
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p✝ q✝ p q : R[X]
hq : ¬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✝ p q : R[X]
hq : ¬q = 0
⊢ degree (p / q) ≤ degree p
rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq]
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p✝ q✝ p q : R[X]
hq : ¬q = 0
⊢ degree (p /ₘ (q * ↑C (leadingCoeff q)⁻¹)) ≤ degree p
exact degree_divByMonic_le _ _