Characteristic polynomial #
Main result #
LinearMap.charpoly_toMatrix f:charpoly fis the characteristic polynomial of the matrix offin any basis.
@[simp]
theorem
LinearMap.charpoly_toMatrix
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[Nontrivial R]
[AddCommGroup M]
[Module R M]
[Module.Free R M]
[Module.Finite R M]
(f : M →ₗ[R] M)
{ι : Type w}
[DecidableEq ι]
[Fintype ι]
(b : Basis ι R M)
:
((LinearMap.toMatrix b b) f).charpoly = f.charpoly
charpoly f is the characteristic polynomial of the matrix of f in any basis.
theorem
LinearMap.charpoly_prodMap
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
[CommRing R]
[Nontrivial R]
[AddCommGroup M₁]
[Module R M₁]
[Module.Finite R M₁]
[Module.Free R M₁]
[AddCommGroup M₂]
[Module R M₂]
[Module.Finite R M₂]
[Module.Free R M₂]
(f₁ : M₁ →ₗ[R] M₁)
(f₂ : M₂ →ₗ[R] M₂)
:
@[simp]
theorem
LinearEquiv.charpoly_conj
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
[CommRing R]
[Nontrivial R]
[AddCommGroup M₁]
[Module R M₁]
[Module.Finite R M₁]
[Module.Free R M₁]
[AddCommGroup M₂]
[Module R M₂]
[Module.Finite R M₂]
[Module.Free R M₂]
(e : M₁ ≃ₗ[R] M₂)
(φ : Module.End R M₁)
:
LinearMap.charpoly (e.conj φ) = LinearMap.charpoly φ