The characteristic polynomial of base change #
@[simp]
theorem
LinearMap.charpoly_baseChange
{R : Type u_3}
{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_1)
[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_3}
{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_1}
[CommRing A]
[Algebra R A]
:
LinearMap.det (baseChange A f) = (algebraMap R A) (LinearMap.det f)
theorem
LinearEquiv.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)
:
LinearEquiv.det (baseChange R A M M f) = (Units.map ↑(algebraMap R A)) (LinearEquiv.det f)
Also see LinearMap.trace_baseChange in Mathlib/LinearAlgebra/Trace