R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.660965
h : leadingCoeff p * leadingCoeff q ≠ 0
⊢ coeff (p * q) (natDegree (p * q)) = coeff p (natDegree p) * coeff q (natDegree q)
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.660965
h : leadingCoeff p * leadingCoeff q ≠ 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
unfold leadingCoeff
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.660965
h : leadingCoeff p * leadingCoeff q ≠ 0
⊢ leadingCoeff p * leadingCoeff q = coeff p (natDegree p) * coeff q (natDegree q)
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.660965
h : leadingCoeff p * leadingCoeff q ≠ 0
⊢ coeff (p * q) (natDegree (p * q)) = coeff p (natDegree p) * coeff q (natDegree q)
rw [natDegree_mul' h, coeff_mul_degree_add_degree]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.660965
h : leadingCoeff p * leadingCoeff q ≠ 0
⊢ leadingCoeff p * leadingCoeff q = coeff p (natDegree p) * coeff q (natDegree q)
rfl