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
n : ℕ
⊢ ∑ n_1 in support p, coeff (↑(RingHom.comp C f) (coeff p n_1) * X ^ n_1) n = ↑f (coeff p n)
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
n : ℕ
⊢ coeff (map f p) n = ↑f (coeff p n)
rw [map, eval₂_def, coeff_sum, sum]
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
n : ℕ
⊢ ∑ n_1 in support p, coeff (↑(RingHom.comp C f) (coeff p n_1) * X ^ n_1) n =
    ∑ x in support p, ↑f (coeff (↑C (coeff p x) * X ^ x) n)
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
n : ℕ
⊢ ∑ n_1 in support p, coeff (↑(RingHom.comp C f) (coeff p n_1) * X ^ n_1) n = ↑f (coeff p n)
conv_rhs => rw [← sum_C_mul_X_pow_eq p, coeff_sum, sum, map_sum]
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
n x : ℕ
_hx : x ∈ support p
⊢ coeff (↑(RingHom.comp C f) (coeff p x) * X ^ x) n = ↑f (coeff (↑C (coeff p x) * X ^ x) n)
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
n : ℕ
⊢ ∑ n_1 in support p, coeff (↑(RingHom.comp C f) (coeff p n_1) * X ^ n_1) n =
    ∑ x in support p, ↑f (coeff (↑C (coeff p x) * X ^ x) n)
refine' Finset.sum_congr rfl fun x _hx => _
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
n x : ℕ
_hx : x ∈ support p
⊢ (if n = x then ↑f (coeff p x) else 0) = ↑f (if n = x then coeff p x else 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
n x : ℕ
_hx : x ∈ support p
⊢ coeff (↑(RingHom.comp C f) (coeff p x) * X ^ x) n = ↑f (coeff (↑C (coeff p x) * X ^ x) n)
simp [Function.comp, coeff_C_mul_X_pow, - map_mul, - coeff_C_mul]
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
n x : ℕ
_hx : x ∈ support p
⊢ (if n = x then ↑f (coeff p x) else 0) = ↑f (if n = x then coeff p x else 0)
split_ifs <;> simp [f.map_zero]