R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.2133490
B' : Type ?u.2133493
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
M : Type u_1
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ ↑(sum p fun e a => ↑(algebraMap R (M →ₗ[R] M)) a * f ^ e) v = sum p fun n b => b • ↑(f ^ n) v
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.2133490
B' : Type ?u.2133493
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
M : Type u_1
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ ↑(↑(aeval f) p) v = sum p fun n b => b • ↑(f ^ n) v
rw [aeval_def, eval₂_eq_sum]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.2133490
B' : Type ?u.2133493
a b : R
n : ℕ
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B'
M : Type u_1
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ ↑(sum p fun e a => ↑(algebraMap R (M →ₗ[R] M)) a * f ^ e) v = sum p fun n b => b • ↑(f ^ n) v
exact (LinearMap.applyₗ v).map_sum