Characteristic polynomial #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main result #
linear_map.charpoly_to_matrix f:charpoly fis the characteristic polynomial of the matrix offin any basis.
@[simp]
theorem
linear_map.charpoly_to_matrix
{R : Type u}
{M : Type v}
[comm_ring R]
[nontrivial R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M]
(f : M →ₗ[R] M)
{ι : Type w}
[fintype ι]
(b : basis ι R M) :
(⇑(linear_map.to_matrix b b) f).charpoly = f.charpoly
charpoly f is the characteristic polynomial of the matrix of f in any basis.