LinearMap.charpoly_toMatrix

theorem LinearMap.charpoly_toMatrix : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : Nontrivial R] [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : Module.Free R M] [inst_5 : Module.Finite R M] (f : M →ₗ[R] M) {ι : Type w} [inst_6 : DecidableEq ι] [inst_7 : Fintype ι] (b : Basis ι R M), ((LinearMap.toMatrix b b) f).charpoly = f.charpoly

The theorem `LinearMap.charpoly_toMatrix` asserts that for any given commutative ring `R`, a non-trivial element of `R`, an additive commutative group `M`, and a linear map `f` from `M` to `M`, where `M` is a free and finite `R`-module, the characteristic polynomial of the matrix representation of `f` (computed via the `LinearMap.toMatrix` function) in any basis `b` (which is a basis of `M` over `R` where the type of indices `ι` is a finite type with decidable equality) is equal to the characteristic polynomial of `f` itself. This means that the characteristic polynomial is invariant under change of basis and is a property of the linear map `f` itself, not the choice of basis.

More concisely: For any commutative ring R, a non-trivial linear map f from a free and finite R-module M to M, and any basis b of M over R, the characteristic polynomials of f and its matrix representation with respect to basis b are equal.