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} {M : Type v} [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.