no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.658581
hq : Monic q
hp : p = 0
⊢ degree (p * q) = degree p + degree q
simp [hp]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.658581
hq : Monic q
hp : ¬p = 0
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
rwa [hq.leadingCoeff, mul_one, Ne.def, leadingCoeff_eq_zero]