proposition: Lemma minpoly_mx1 : (1%:M \in Ad)%MS.
proof: Proof. by apply: (eq_row_sub (Ordinal mxminpoly_nonconstant)); rewrite rowK. 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)