proposition: Lemma Frobenius_seq_neq0 n (A : 'M[F]_n) p : p \in Frobenius_seq A -> p != 0.
proof: Proof. have Hc := (Frobenius_seq_char_poly A). have: char_poly A != 0. by rewrite -size_poly_eq0 size_char_poly. rewrite -Hc (big_nth 0) big_mkord. move/prodf_neq0=> H0 /(nthP 0) [i Hi] <-. exact: (H0 (Ordinal Hi)). 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)