proposition: Lemma similar_Frobenius n (A : 'M[R]_n.+1) : similar (Frobenius_form A) (Frobenius_form_CF A).
proof: Proof. rewrite /Frobenius_form /Frobenius_form_CF. move: (@monic_invariant_factors _ _ A). have: forall p, p \in (invariant_factors A) -> (1 < size p)%N. by move=> p; rewrite mem_filter; case/andP. case: (invariant_factors A)=>[_ _|a l]; first exact: similar_refl. elim: l a=> /= [a Hsa Hma |b l IHl a Hs Hm]. rewrite !cats0; apply: similar_poly_inv. by rewrite Hsa // mem_head. by rewrite Hma // mem_head. have IHs: forall p : {poly R}, p \in b :: l -> (1 < size p)%N. by move=> p Hp; apply: Hs; rewrite mem_behead. have IHm: forall p : {poly R}, p \in b :: l -> p \is monic. by move=> p HP; apply: Hm; rewrite mem_behead. have Hsa: (1 < size a)%N by rewrite Hs // mem_head. have Hma: a \is monic by rewrite Hm // mem_head. set M := companion_mxn _ _. apply: (similar_trans (similar_drblockmx M (IHl b IHs IHm))). apply: (similar_trans (similar_ulblockmx _ (similar_poly_inv Hsa Hma))). have Hnv: forall p, p \in [:: a, b & l] -> linear_factor_seq p != [::]. move=> p Hp; rewrite /linear_factor_seq -size_eq0 !size_map size_eq0. rewrite /root_seq_uniq; apply: contra_neq; first exact: undup_nil. by rewrite -root_seq_nil -ltnNge; apply: Hs. set s1 := _ ++ _. set s2 := linear_factor_seq _ ++ _. have: (linear_factor_seq a) != [::] by rewrite Hnv // mem_head. have t: s2 != [::]. have: linear_factor_seq b != [::] by rewrite Hnv // mem_behead // mem_head. by rewrite /s2; case: (linear_factor_seq b). clear -t. have ->: s1 = [seq (size p).-2 | p : {poly R} <- s2]. by rewrite /s1 map_cat map_flatten; congr (_ ++ _); rewrite [in LHS]map_comp. case: (linear_factor_seq a)=> //= c s _. elim: s c=> [c|c s IHs d] /=. case: s2 t => // d s2 _ /=. exact: similar_refl. set M := companion_mxn _ _. apply: similar_sym. apply: (similar_trans (similar_drblockmx M (similar_sym (IHs c)))). rewrite /GRing.zero /= -row_mx_const -col_mx_const block_mxA. apply/similar_sym/similar_cast. rewrite col_mx_const row_mx_const. 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)