R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f✝ : R →+* S
x✝ : S
f : R →+* S
p : R[X]
n : ℕ
hn : natDegree p < n
x : S
⊢ ∀ (n : ℕ), ↑f 0 * x ^ n = 0
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f✝ : R →+* S
x✝ : S
f : R →+* S
p : R[X]
n : ℕ
hn : natDegree p < n
x : S
⊢ eval₂ f x p = ∑ i in range n, ↑f (coeff p i) * x ^ i
rw [eval₂_eq_sum, p.sum_over_range' _ _ hn]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f✝ : R →+* S
x✝ : S
f : R →+* S
p : R[X]
n : ℕ
hn : natDegree p < n
x : S
i : ℕ
⊢ ↑f 0 * x ^ i = 0
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f✝ : R →+* S
x✝ : S
f : R →+* S
p : R[X]
n : ℕ
hn : natDegree p < n
x : S
⊢ ∀ (n : ℕ), ↑f 0 * x ^ n = 0
intro i
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f✝ : R →+* S
x✝ : S
f : R →+* S
p : R[X]
n : ℕ
hn : natDegree p < n
x : S
i : ℕ
⊢ ↑f 0 * x ^ i = 0
rw [f.map_zero, zero_mul]