no goals
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
k : ℕ
⊢ f ^ k = ↑(aeval f) (X ^ k %ₘ charpoly f)
rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]