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.
