R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type ?u.272359
B' : Type ?u.272362
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
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : R[X]
f : A →ₐ[R] B
a : A
⊢ ↑f (∑ n in support p, ↑(algebraMap R A) (coeff p n) * a ^ n) =
    ∑ n in support p, ↑(algebraMap R B) (coeff p n) * ↑f a ^ n
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type ?u.272359
B' : Type ?u.272362
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
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : R[X]
f : A →ₐ[R] B
a : A
⊢ ↑f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (↑f a) p
simp only [eval₂_eq_sum, sum_def]
no goals
R✝ : Type u
S : Type v
T : Type w
A✝ : Type z
A' : Type ?u.272359
B' : Type ?u.272362
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
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : R[X]
f : A →ₐ[R] B
a : A
⊢ ↑f (∑ n in support p, ↑(algebraMap R A) (coeff p n) * a ^ n) =
    ∑ n in support p, ↑(algebraMap R B) (coeff p n) * ↑f a ^ n
simp only [f.map_sum, f.map_mul, f.map_pow, eq_intCast, map_intCast, AlgHom.commutes]