# mathlibdocumentation

linear_algebra.charpoly.to_matrix

# Characteristic polynomial #

## Main result #

• linear_map.charpoly_to_matrix f : charpoly f is the characteristic polynomial of the matrix of f in any basis.
@[simp]
theorem linear_map.charpoly_to_matrix {R : Type u} {M : Type v} [comm_ring R] [nontrivial R] [ M] [ M] [ M] (f : M →ₗ[R] M) {ι : Type w} [fintype ι] (b : R M) :

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