mathlib3 documentation


Characteristic polynomial #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main result #

theorem linear_map.charpoly_to_matrix {R : Type u} {M : Type v} [comm_ring R] [nontrivial R] [add_comm_group M] [module R M] [ R M] [module.finite R M] (f : M →ₗ[R] M) {ι : Type w} [fintype ι] (b : basis ι R M) :

charpoly f is the characteristic polynomial of the matrix of f in any basis.