R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1271761
B' : Type ?u.1271764
a b : R
n : ℕ
inst✝⁸ : CommSemiring A'
inst✝⁷ : Semiring B'
inst✝⁶ : CommSemiring R
p✝ q : R[X]
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type ?u.1271977
inst✝³ : Semiring B
inst✝² : Algebra R B
x✝ : A
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Algebra R S
p : R[X]
x : S
⊢ ↑(aeval x) p = ∑ x_1 in range (natDegree p + 1), ↑(algebraMap R S) (coeff p x_1) * x ^ x_1
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1271761
B' : Type ?u.1271764
a b : R
n : ℕ
inst✝⁸ : CommSemiring A'
inst✝⁷ : Semiring B'
inst✝⁶ : CommSemiring R
p✝ q : R[X]
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type ?u.1271977
inst✝³ : Semiring B
inst✝² : Algebra R B
x✝ : A
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Algebra R S
p : R[X]
x : S
⊢ ↑(aeval x) p = ∑ i in range (natDegree p + 1), coeff p i • x ^ i
simp_rw [Algebra.smul_def]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1271761
B' : Type ?u.1271764
a b : R
n : ℕ
inst✝⁸ : CommSemiring A'
inst✝⁷ : Semiring B'
inst✝⁶ : CommSemiring R
p✝ q : R[X]
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type ?u.1271977
inst✝³ : Semiring B
inst✝² : Algebra R B
x✝ : A
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Algebra R S
p : R[X]
x : S
⊢ ↑(aeval x) p = ∑ x_1 in range (natDegree p + 1), ↑(algebraMap R S) (coeff p x_1) * x ^ x_1
exact eval₂_eq_sum_range (algebraMap R S) x