proposition: Lemma Frobenius_seq_char_poly n (A : 'M[F]_n) : \prod_(p <- Frobenius_seq A) p = char_poly A.
proof: Proof. rewrite big_map scaler_prod prodfV. have Hs m (B : 'M[F]_m): size (take m (Smith_seq (char_poly_mx B))) = m. by move: (size_Frobenius_seq B); rewrite size_map. have Hp1: \prod_(i <- (take n (Smith_seq (char_poly_mx A)))) i = char_poly A. case: n A => [A| n A]; first by rewrite big_nil /char_poly det_mx00. rewrite -(det_diag_mx_seq (Hs _ A)). by rewrite diag_mx_seq_takel det_Smith. have ->: \prod_(i <- (take n (Smith_seq (char_poly_mx A)))) lead_coef i = 1. rewrite lead_coef_prod Hp1. by apply/monicP/char_poly_monic. by rewrite Hp1 invr1 scale1r. 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)