proposition: Lemma equiv_Frobenius_seq n (A : 'M[F]_n) : equivalent (diag_mx_seq n n (Smith_seq (char_poly_mx A))) (diag_mx_seq n n (Frobenius_seq A)).
proof: Proof. rewrite -diag_mx_seq_takel. apply: eqd_equiv=> // [|i]; first by rewrite size_map. set s := take _ _. case: (ltnP i (size s)) => Hi; last by rewrite !nth_default // size_map. rewrite (nth_map 0) //; apply/eqdP. exists ((lead_coef s`_i)^-1%:P). have Hin: (Frobenius_seq A)`_i \in Frobenius_seq A. by rewrite mem_nth // size_map. have:= Frobenius_seq_neq0 Hin. rewrite (nth_map 0) // scaler_eq0 negb_or=> /andP [Hl _]. by rewrite rmorph_unit // unitfE. by rewrite mul_polyC. 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)