R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
have hp : p ≠ 0 := fun hp => h (by rw [hp, zero_mul])
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
have hq : q ≠ 0 := fun hq => h (by rw [hq, mul_zero])
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
have : ∀ (p : R[X]), WithTop.some (natTrailingDegree p) = Nat.cast (natTrailingDegree p) :=
  fun p ↦ rfl
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ trailingDegree p + trailingDegree q ≤ trailingDegree (p * q)
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
rw [← WithTop.coe_le_coe, WithTop.coe_add, this p, this q, this (p * q),
  ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq,
  ← trailingDegree_eq_natTrailingDegree h]
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ trailingDegree p + trailingDegree q ≤ trailingDegree (p * q)
exact le_trailingDegree_mul
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p = 0
⊢ p * q = 0
rw [hp, zero_mul]
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p * q = 0
rw [hq, mul_zero]