proposition: Lemma dvdp_invf_char_poly m (A : 'M[F]_m) (p : {poly F}) : p \in (invariant_factors A) -> dvdp p (char_poly A).
proof: Proof. move=> Hp. rewrite -invf_char_poly prod_seq_count. have Hi: p \in undup (invariant_factors A) by rewrite mem_undup. rewrite (bigD1_seq _ Hi) ?undup_uniq //= dvdp_mulr // dvdp_exp //. by rewrite -has_count has_pred1. 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)