proposition: Lemma kermxpolyC n (g : 'M_n) c : c != 0 -> kermxpoly g c%:P = 0.
proof: Proof. move=> c_neq0; case: n => [|n] in g *; first by rewrite thinmx0. apply/eqP; rewrite /kermxpoly horner_mx_C kermx_eq0 row_free_unit. by rewrite -scalemx1 scaler_unit ?unitmx1// unitfE. 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)