R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.656983
h : leadingCoeff p * leadingCoeff q ≠ 0
⊢ p = 0 → leadingCoeff p * leadingCoeff q = 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.656983
h : leadingCoeff p * leadingCoeff q ≠ 0
⊢ p ≠ 0
refine' mt _ h
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.656983
h : leadingCoeff p * leadingCoeff q ≠ 0
⊢ p = 0 → leadingCoeff p * leadingCoeff q = 0
exact fun hp => by rw [hp, leadingCoeff_zero, zero_mul]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.656983
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p = 0
⊢ leadingCoeff p * leadingCoeff q = 0
rw [hp, leadingCoeff_zero, zero_mul]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.656983
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
⊢ q = 0 → leadingCoeff p * leadingCoeff q = 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.656983
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
⊢ q ≠ 0
refine' mt _ h
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.656983
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
⊢ q = 0 → leadingCoeff p * leadingCoeff q = 0
exact fun hq => by rw [hq, leadingCoeff_zero, mul_zero]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.656983
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ leadingCoeff p * leadingCoeff q = 0
rw [hq, leadingCoeff_zero, mul_zero]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.656983
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ↑(natDegree p) + ↑(natDegree q) ≤ degree (p * q)
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.656983
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ degree p + degree q ≤ degree (p * q)
rw [degree_eq_natDegree hp, degree_eq_natDegree hq]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.656983
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ coeff (p * q) (natDegree p + natDegree q) ≠ 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.656983
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ↑(natDegree p) + ↑(natDegree q) ≤ degree (p * q)
refine le_degree_of_ne_zero (n := natDegree p + natDegree q) ?_
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.656983
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ coeff (p * q) (natDegree p + natDegree q) ≠ 0
rwa [coeff_mul_degree_add_degree]