case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : q = 0
⊢ natDegree (p * q) = natDegree (q * p)

case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ natDegree (p * q) = natDegree (q * p)
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
⊢ natDegree (p * q) = natDegree (q * p)
by_cases h : q = 0
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ Polynomial.leadingCoeff q * Polynomial.leadingCoeff p ≠ 0
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ natDegree (p * q) = natDegree (q * p)
rw [hp.natDegree_mul' h, Polynomial.natDegree_mul', add_comm]
no goals
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ Polynomial.leadingCoeff q * Polynomial.leadingCoeff p ≠ 0
simpa [hp.leadingCoeff, leadingCoeff_ne_zero]
no goals
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : q = 0
⊢ natDegree (p * q) = natDegree (q * p)
simp [h]