proposition: Lemma invf_char_poly n (A : 'M[F]_n) : \prod_(p <- invariant_factors A) p = char_poly A.
proof: Proof. rewrite -Frobenius_seq_char_poly Frobenius_seqE. rewrite big_cat /= (big1_seq (nseq _ _)) ?mul1r // => i. case/andP=> _ /(nthP 0) [j]. by rewrite size_nseq=> Hj; rewrite nth_nseq Hj=> ->. 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)