R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ natDegree (p * q) = natDegree p + natDegree q
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
⊢ natDegree (p * q) = natDegree p + natDegree q
nontriviality R
case h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ natDegree (p * q) = natDegree p + natDegree q
apply natDegree_mul'
no goals
case h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
simp [hp.leadingCoeff, hq.leadingCoeff]