R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ ↑C (coeff p (natDegree p)) * X ^ natDegree p + ∑ x in range (natDegree p), ↑C (coeff p x) * X ^ x =
    X ^ natDegree p + ∑ i in range (natDegree p), ↑C (coeff p i) * X ^ i
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ p = X ^ natDegree p + ∑ i in range (natDegree p), ↑C (coeff p i) * X ^ i
conv_lhs => rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ ↑C (coeff p (natDegree p)) = 1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ ↑C (coeff p (natDegree p)) * X ^ natDegree p + ∑ x in range (natDegree p), ↑C (coeff p x) * X ^ x =
    X ^ natDegree p + ∑ i in range (natDegree p), ↑C (coeff p i) * X ^ i
suffices C (p.coeff p.natDegree) = 1 by rw [this, one_mul]
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ ↑C (coeff p (natDegree p)) = 1
exact congr_arg C hp
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
this : ↑C (coeff p (natDegree p)) = 1
⊢ ↑C (coeff p (natDegree p)) * X ^ natDegree p + ∑ x in range (natDegree p), ↑C (coeff p x) * X ^ x =
    X ^ natDegree p + ∑ i in range (natDegree p), ↑C (coeff p i) * X ^ i
rw [this, one_mul]