Commit 2021-10-02 16:08 110c740c

refactor(linear_algebra/charpoly): split in two files (#9485) We split linear_algebra/charpoly in linear_algebra/charpoly/basic and linear_algebra/charpoly/to_matrix. Currently in linear_algebra/charpoly/to_matrix we only prove linear_map.charpoly_to_matrix f : charpoly f is the characteristic polynomial of the matrix of f in any basis. This needs to be in a separate file then the definition of f.charpoly since it needs the invariant basis number property for commutative rings and in a future PR I will prove this as a special case of the fact that any commutative ring satisfies the strong rank condition, but the proof of this uses the characteristic polynomial. We plan to add ohter results regarding the characteristic polynomial in the future.