proposition: Lemma map_geigenspace (n : nat) (g : 'M_n) (a : aF) : map_mx f (geigenspace g a) = geigenspace (map_mx f g) (f a).
proof: Proof. by rewrite map_kermxpoly rmorphXn/= rmorphB /= map_polyX map_polyC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)