proposition: Lemma Jordan n (A : 'M[R]_n.+1) : similar A (Jordan_form A).
proof: Proof. apply: (similar_trans (Frobenius _)). apply: (similar_trans (similar_Frobenius _)). rewrite /Frobenius_form_CF /Jordan_form /root_seq_poly /linear_factor_seq. set s1 := flatten _. set s2 := map _ _. have Hs: size s1 = size s2. rewrite /s1 size_map. by do 2! rewrite map_comp -map_flatten size_map. apply: similar_diag_block=> // i; rewrite /s1. (do 2! rewrite map_comp -map_flatten size_map) => Hi. rewrite (nth_map 0) ?size_map //. rewrite !(nth_map (0,0%N)) ?size_map //. set x := nth _ _ _. rewrite -(@prednK x.2); first exact: similar_cj. have/flattenP [s Hfs Hx] := mem_nth (0,0%N) Hi; move: Hfs. case/(nthP nil)=> m; rewrite !size_map=> Hm Heq. move: Heq Hx; rewrite (nth_map 0) // => <-. apply: root_mu_seq_pos. apply: (@invariant_factor_neq0 _ _ A). by rewrite mem_nth. 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) CoqEAL(frobenius_form)