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 : ℕ
a : R
⊢ eval₂ (RingHom.comp C f) X (↑(monomial n) a) = ↑(monomial n) (↑f a)
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 : ℕ
a : R
⊢ map f (↑(monomial n) a) = ↑(monomial n) (↑f a)
dsimp only [map]
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 : ℕ
a : R
⊢ ↑(RingHom.comp C f) a * X ^ n = ↑C (↑f a) * 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 : ℕ
a : R
⊢ eval₂ (RingHom.comp C f) X (↑(monomial n) a) = ↑(monomial n) (↑f a)
rw [eval₂_monomial, ← C_mul_X_pow_eq_monomial]
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 : ℕ
a : R
⊢ ↑(RingHom.comp C f) a * X ^ n = ↑C (↑f a) * X ^ n
rfl