case ofFinsupp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
hf : ∀ (k : ℕ), Commute (↑f (coeff q k)) x
p : AddMonoidAlgebra R ℕ
⊢ eval₂ f x ({ toFinsupp := p } * q) = eval₂ f x { toFinsupp := p } * eval₂ f x q
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
hf : ∀ (k : ℕ), Commute (↑f (coeff q k)) x
⊢ eval₂ f x (p * q) = eval₂ f x p * eval₂ f x q
rcases p with ⟨p⟩
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
p q : AddMonoidAlgebra R ℕ
hf : ∀ (k : ℕ), Commute (↑f (coeff { toFinsupp := q } k)) x
⊢ eval₂ f x ({ toFinsupp := p } * { toFinsupp := q }) = eval₂ f x { toFinsupp := p } * eval₂ f x { toFinsupp := q }
case ofFinsupp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
hf : ∀ (k : ℕ), Commute (↑f (coeff q k)) x
p : AddMonoidAlgebra R ℕ
⊢ eval₂ f x ({ toFinsupp := p } * q) = eval₂ f x { toFinsupp := p } * eval₂ f x q
rcases q with ⟨q⟩
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
p q : AddMonoidAlgebra R ℕ
hf : ∀ (k : ℕ), Commute (↑f (↑q k)) x
⊢ eval₂ f x ({ toFinsupp := p } * { toFinsupp := q }) = eval₂ f x { toFinsupp := p } * eval₂ f x { toFinsupp := q }
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
p q : AddMonoidAlgebra R ℕ
hf : ∀ (k : ℕ), Commute (↑f (coeff { toFinsupp := q } k)) x
⊢ eval₂ f x ({ toFinsupp := p } * { toFinsupp := q }) = eval₂ f x { toFinsupp := p } * eval₂ f x { toFinsupp := q }
simp only [coeff] at hf
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
p q : AddMonoidAlgebra R ℕ
hf : ∀ (k : ℕ), Commute (↑f (↑q k)) x
⊢ ↑(liftNC ↑f ↑(↑(powersHom S) x)) (p * q) = ↑(liftNC ↑f ↑(↑(powersHom S) x)) p * ↑(liftNC ↑f ↑(↑(powersHom S) x)) q
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
p q : AddMonoidAlgebra R ℕ
hf : ∀ (k : ℕ), Commute (↑f (↑q k)) x
⊢ eval₂ f x ({ toFinsupp := p } * { toFinsupp := q }) = eval₂ f x { toFinsupp := p } * eval₂ f x { toFinsupp := q }
simp only [← ofFinsupp_mul, eval₂_ofFinsupp]
no goals
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
p q : AddMonoidAlgebra R ℕ
hf : ∀ (k : ℕ), Commute (↑f (↑q k)) x
⊢ ↑(liftNC ↑f ↑(↑(powersHom S) x)) (p * q) = ↑(liftNC ↑f ↑(↑(powersHom S) x)) p * ↑(liftNC ↑f ↑(↑(powersHom S) x)) q
exact liftNC_mul _ _ p q fun {k n} _hn => (hf k).pow_right n