proposition: Lemma mxminpoly_linear_is_scalar : (d <= 1) = is_scalar_mx A.
proof: Proof. have scalP := has_non_scalar_mxP minpoly_mx1. rewrite leqNgt -(eqnP minpoly_mx_free); apply/scalP/idP=> [|[[B]]]. case scalA: (is_scalar_mx A); [by right | left]. by exists A; rewrite ?scalA // -{1}(horner_mx_X A) horner_mx_mem. move/mx_inv_hornerK=> <- nsB; case/is_scalar_mxP=> a defA; case/negP: nsB. move: {B}(_ B); apply: poly_ind => [|p c]. by rewrite rmorph0 ?mx0_is_scalar. rewrite rmorphD ?rmorphM /= horner_mx_X defA; case/is_scalar_mxP=> b ->. by rewrite -rmorphM horner_mx_C -rmorphD /= scalar_mx_is_scalar. 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)