The characteristic polynomial of base change

@[simp]

theorem LinearMap.charpoly_baseChange {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) (A : Type u_3) [CommRing A] [Algebra R A] : (baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly

theorem LinearMap.det_eq_sign_charpoly_coeff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) : LinearMap.det f = (-1) ^ Module.finrank R M * f.charpoly.coeff 0

theorem LinearMap.det_baseChange {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {A : Type u_3} [CommRing A] [Algebra R A] (f : M →ₗ[R] M) : LinearMap.det (baseChange A f) = (algebraMap R A) (LinearMap.det f)

Also see LinearMap.trace_baseChange in Mathlib/LinearAlgebra/Trace