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
x : S
inst✝ : Semiring T
h : Commute (↑f a) x
⊢ ∀ (k : ℕ), Commute (↑f (coeff (↑C a) 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
h : Commute (↑f a) x
⊢ eval₂ f x (p * ↑C a) = eval₂ f x p * ↑f a
rw [eval₂_mul_noncomm, eval₂_C]
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
x : S
inst✝ : Semiring T
h : Commute (↑f a) x
k : ℕ
⊢ Commute (↑f (coeff (↑C a) k)) x
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
x : S
inst✝ : Semiring T
h : Commute (↑f a) x
⊢ ∀ (k : ℕ), Commute (↑f (coeff (↑C a) k)) x
intro k
case pos
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
h : Commute (↑f a) x
k : ℕ
hk : k = 0
⊢ Commute (↑f (coeff (↑C a) k)) x

case neg
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
h : Commute (↑f a) x
k : ℕ
hk : ¬k = 0
⊢ Commute (↑f (coeff (↑C a) k)) x
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
x : S
inst✝ : Semiring T
h : Commute (↑f a) x
k : ℕ
⊢ Commute (↑f (coeff (↑C a) k)) x
by_cases hk : k = 0
no goals
case pos
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
h : Commute (↑f a) x
k : ℕ
hk : k = 0
⊢ Commute (↑f (coeff (↑C a) k)) x
simp only [hk, h, coeff_C_zero, coeff_C_ne_zero]
no goals
case neg
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
h : Commute (↑f a) x
k : ℕ
hk : ¬k = 0
⊢ Commute (↑f (coeff (↑C a) k)) x
simp only [coeff_C_ne_zero hk, RingHom.map_zero, Commute.zero_left]