case hf
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
⊢ ∀ (k : ℕ), Commute (↑(RingHom.comp C f) (coeff q k)) X
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
⊢ map f (p * q) = map f p * map f q
rw [map, eval₂_mul_noncomm]
no goals
case hf
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
⊢ ∀ (k : ℕ), Commute (↑(RingHom.comp C f) (coeff q k)) X
exact fun k => (commute_X _).symm