R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p✝ q p : R[X]
hq : q ≠ 0
⊢ degree (mod p q) < degree (q * ↑C (leadingCoeff q)⁻¹)
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p✝ q p : R[X]
hq : q ≠ 0
⊢ degree (mod p q) < degree q
rw [← degree_mul_leadingCoeff_inv q 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 : R[X]
hq : q ≠ 0
⊢ degree (mod p q) < degree (q * ↑C (leadingCoeff q)⁻¹)
exact degree_modByMonic_lt p (monic_mul_leadingCoeff_inv hq)