R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type ?u.303170
B' : Type ?u.303173
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ eval₂ (algebraMap R A) (↑f X) p = ↑f (sum p fun n a => ↑C a * X ^ n)
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type ?u.303170
B' : Type ?u.303173
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ eval₂ (algebraMap R A) (↑f X) p = ↑f p
conv_rhs => rw [← Polynomial.sum_C_mul_X_pow_eq p]
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type ?u.303170
B' : Type ?u.303173
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ ∑ n in support p, ↑(algebraMap R A) (coeff p n) * ↑f X ^ n = ↑f (∑ n in support p, ↑C (coeff p n) * X ^ n)
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type ?u.303170
B' : Type ?u.303173
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ eval₂ (algebraMap R A) (↑f X) p = ↑f (sum p fun n a => ↑C a * X ^ n)
simp only [eval₂_eq_sum, sum_def]
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type ?u.303170
B' : Type ?u.303173
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ ∑ n in support p, ↑(algebraMap R A) (coeff p n) * ↑f X ^ n = ∑ x in support p, ↑f (↑C (coeff p x)) * ↑f X ^ x
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type ?u.303170
B' : Type ?u.303173
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ ∑ n in support p, ↑(algebraMap R A) (coeff p n) * ↑f X ^ n = ↑f (∑ n in support p, ↑C (coeff p n) * X ^ n)
simp only [f.map_sum, f.map_mul, f.map_pow, eq_intCast, map_intCast]
no goals
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type ?u.303170
B' : Type ?u.303173
a b : R✝
n : ℕ
inst✝⁷ : CommSemiring A'
inst✝⁶ : Semiring B'
inst✝⁵ : CommSemiring R✝
p✝ q r : R✝[X]
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ ∑ n in support p, ↑(algebraMap R A) (coeff p n) * ↑f X ^ n = ∑ x in support p, ↑f (↑C (coeff p x)) * ↑f X ^ x
simp [Polynomial.C_eq_algebraMap]