R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ trailingDegree (p * q) ≤ trailingDegree p + trailingDegree q
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
refine' le_antisymm _ le_trailingDegree_mul
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ trailingDegree (p * q) ≤ ↑(natTrailingDegree p + natTrailingDegree q)
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ trailingDegree (p * q) ≤ trailingDegree p + trailingDegree q
rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq, ←
  ENat.coe_add]
case h
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ coeff (p * q) (natTrailingDegree p + natTrailingDegree q) ≠ 0
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ trailingDegree (p * q) ≤ ↑(natTrailingDegree p + natTrailingDegree q)
apply le_trailingDegree_of_ne_zero
no goals
case h
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ coeff (p * q) (natTrailingDegree p + natTrailingDegree q) ≠ 0
rwa [coeff_mul_natTrailingDegree_add_natTrailingDegree]
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p = 0
⊢ trailingCoeff p * trailingCoeff q = 0
rw [hp, trailingCoeff_zero, zero_mul]
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ trailingCoeff p * trailingCoeff q = 0
rw [hq, trailingCoeff_zero, mul_zero]