proposition: Lemma minpoly_mx_ring : mxring Ad.
proof: Proof. apply/andP; split; first exact/mulsmx_subP/minpoly_mxM. apply/mxring_idP; exists 1%:M; split=> *; rewrite ?mulmx1 ?mul1mx //. by rewrite -mxrank_eq0 mxrank1. exact: minpoly_mx1. 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)