Characteristic polynomial

Main result

• LinearMap.charpoly_toMatrix f : charpoly f is the characteristic polynomial of the matrix of f in 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) : Matrix.charpoly ((LinearMap.toMatrix b b) f) = LinearMap.charpoly f

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₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Module.Finite R M₁] [Module.Finite R M₂] [Module.Free R M₁] [Module.Free R M₂] (f₁ : M₁ →ₗ[R] M₁) (f₂ : M₂ →ₗ[R] M₂) : LinearMap.charpoly (LinearMap.prodMap f₁ f₂) = LinearMap.charpoly f₁ * LinearMap.charpoly f₂