General linear group characteristic polynomial helpers

This file restores a similarity invariance lemma for matrix characteristic polynomials.

theorem Matrix.charpoly.similar_eq {F : Type u_1} [Field F] (n : ℕ) (u : (Matrix (Fin n) (Fin n) F)ˣ) (A B : Matrix (Fin n) (Fin n) F) (h : A = ↑u * B * ↑u⁻¹) : A.charpoly = B.charpoly