proposition: Lemma mxminpoly_inv_factors n (A : 'M[F]_n.+1) : last 0 (Frobenius_seq A) = mxminpoly A.
proof: Proof. have Hif: (0 < size (invariant_factors A))%N. by rewrite lt0n size_eq0 nnil_inv_factors. have Hfn: [seq (size p).-2 | p : E <- invariant_factors A] != [::]. by rewrite -size_eq0 size_map size_eq0 nnil_inv_factors. apply: mxminpolyP=> [||q HA]. - apply: (@monic_Frobenius_seq _ A). by rewrite -nth_last mem_nth // size_Frobenius_seq. - apply: (similar_horner (similar_sym (Frobenius A))). rewrite horner_mx_diag_block //. apply/diag_block_mx0=> i; rewrite size_map=> Hi. rewrite !(nth_map 0) // Frobenius_seqE last_cat -nth_last. rewrite (set_nth_default 0) ?prednK // ?Hif //. set p := nth _ _ _. apply: (@horner_mx_dvdp _ _ p). apply: sorted_leq_nth=> //. - exact: dvdp_trans. - exact: sorted_invf. - by rewrite inE prednK. by rewrite -ltnS prednK. rewrite -{5}[p]comp_mxminpolyK. - exact: mx_root_minpoly. - exact: (monic_invariant_factors (mem_nth 0 Hi)). move: (mem_nth 0 Hi). by rewrite mem_filter -subn_gt0 subn1; case/andP. move: (similar_horner (Frobenius A) HA). rewrite horner_mx_diag_block // => /diag_block_mx0=> H. rewrite Frobenius_seqE last_cat -nth_last (set_nth_default 0) ?prednK //. move: (H (size (invariant_factors A)).-1). rewrite size_map !(nth_map 0) ?prednK //. set p := nth _ _ _=> Hp. have Hm:= @mem_nth _ 0 (invariant_factors A) (size (invariant_factors A)).-1. rewrite -[p]comp_mxminpolyK ?dvdr_dvdp. - exact: (mxminpoly_min (Hp (leqnn _))). - apply/(@monic_invariant_factors _ A)/Hm. by rewrite prednK // mem_filter -subn_gt0 subn1. move: Hm; rewrite prednK // mem_filter -subn_gt0 subn1=> h. by case/andP: (h (leqnn _)). Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image companion closed_poly smith_complements)