proposition: Lemma Frobenius_unicity n m (A : 'M[F]_n) (B : 'M_m) : similar A B <-> invariant_factors A = invariant_factors B.
proof: Proof. split=> [[Hmn H]|H]; rewrite /invariant_factors. congr filter; apply: (@eq_from_nth _ 0)=>[|i Hi]. by rewrite !size_Frobenius_seq. have/Frobenius_seq_neq0 := mem_nth 0 Hi. rewrite size_Frobenius_seq in Hi. rewrite !(nth_map 0) ?size_Smith_seq -?Hmn -?size_poly_eq0 ?size_char_poly //. rewrite size_poly_eq0 scaler_eq0 negb_or invr_eq0=> /andP [Hl0 _]. apply: (scalerI Hl0); rewrite !scalerA mulrV ?unitfE // scale1r. apply: eqpfP; rewrite /eqp -!dvdr_dvdp [X in take X]Hmn. rewrite Hmn in Hi; rewrite !nth_take //. apply: Smith_unicity => //; first exact: sorted_Smith. set D := char_poly_mx A. rewrite -{3 4 6 7}Hmn. apply: (equiv_trans _ (equiv_Smith D)). by apply/similar_fundamental/similar_sym. have/eqP: n = m. - by rewrite -(sum_size_inv_factors A) -(sum_size_inv_factors B) H. case: n A H => [A|n A]; case: m B=> [B|m B] H Hmn //. exact: similar0. apply/(similar_trans (Frobenius A))/similar_sym/(similar_trans (Frobenius B)). rewrite /Frobenius_form H. exact: similar_refl. 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)