proposition: Lemma invariant_factor_neq0 n (A : 'M[F]_n) : forall p, p \in invariant_factors A -> p != 0.
proof: Proof. by move=> p; rewrite mem_filter; case/andP=> _; exact: Frobenius_seq_neq0. 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)