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
x : S
inst✝ : Semiring T
k : ℕ
⊢ Commute (↑f (coeff X 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
x : S
inst✝ : Semiring T
⊢ eval₂ f x (p * X) = eval₂ f x p * x
refine' _root_.trans (eval₂_mul_noncomm _ _ fun k => _) (by rw [eval₂_X])
case inl
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
x : S
inst✝ : Semiring T
⊢ Commute (↑f (coeff X 1)) x

case inr
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
x : S
inst✝ : Semiring T
k : ℕ
hk : ¬k = 1
⊢ Commute (↑f (coeff X 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
x : S
inst✝ : Semiring T
k : ℕ
⊢ Commute (↑f (coeff X k)) x
rcases em (k = 1) with (rfl | hk)
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
x : S
inst✝ : Semiring T
⊢ eval₂ f x p * eval₂ f x X = eval₂ f x p * x
rw [eval₂_X]
no goals
case inl
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
x : S
inst✝ : Semiring T
⊢ Commute (↑f (coeff X 1)) x
simp
no goals
case inr
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
x : S
inst✝ : Semiring T
k : ℕ
hk : ¬k = 1
⊢ Commute (↑f (coeff X k)) x
simp [coeff_X_of_ne_one hk]