no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp0 : p = 0
⊢ degree (p * q) = degree p + degree q
simp only [hp0, degree_zero, zero_mul, WithBot.bot_add]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp0 : ¬p = 0
hq0 : q = 0
⊢ degree (p * q) = degree p + degree q
simp only [hq0, degree_zero, mul_zero, WithBot.add_bot]