proposition: Lemma diagonalization n (A : 'M[R]_n.+1) : uniq (root_seq (mxminpoly A)) -> similar A (diag_mx_seq n.+1 n.+1 (root_seq (char_poly A))).
proof: Proof. move=> H. have [Heq _]:= Jordan A. pose s := [seq (x.2).-1 | x <- root_seq_poly (invariant_factors A)]. have Hs: size ([seq (Jordan_form A) i i | i <- enum 'I_(size_sum s).+1]) = n.+1. by rewrite size_map size_enum_ord. have Hn i: nth 0%N s i = 0%N. case: (ltnP i (size (root_seq_poly (invariant_factors A))))=> Hi. rewrite (nth_map (0,0%N)) //. have/flattenP [s2 Hd Hs2] := (mem_nth (0,0%N) Hi); move: Hd. case/(nthP nil)=> m; rewrite !size_map=> Hm Heq2. move: Heq2 Hs2; rewrite (nth_map 0) // => <-. move=> Hr; rewrite (uniq_root_mu_seq _ Hr) //. apply: (uniq_root_dvdp _ H). by rewrite monic_neq0 // mxminpoly_monic. rewrite -mxminpoly_inv_factors Frobenius_seqE last_cat -nth_last. have Hif: (0 < (size (invariant_factors A)))%N. by rewrite lt0n size_eq0 nnil_inv_factors. rewrite (set_nth_default 0) ?prednK //. apply: sorted_leq_nth=> //. - exact: dvdp_trans. - exact: sorted_invf. - by rewrite inE prednK. by rewrite -ltnS prednK. by rewrite nth_default // size_map. apply: (similar_trans (Jordan A)). apply: (similar_trans _ (similar_diag_mx_seq (erefl n.+1) Hs (eigen_diag A))). rewrite /Jordan_form diag_block_mx_seq //. rewrite size_map size_enum_ord in Hs. rewrite Hs. set s1 := mkseq _ _. set s2 := map _ _. have ->: s2 = s1. apply: (@eq_from_nth _ 0). rewrite size_map size_enum_ord Heq size_mkseq. rewrite size_sum_big. rewrite (eq_big_seq (fun _ => 1%N)). by rewrite (big_nth 0%N) sum_nat_const_nat subn0 muln1. by move=> x /(nthP 0%N) [i Hi]; rewrite Hn=> <-. rewrite -size_eq0 size_map size_flatten sumn_big !big_map. have H0: (0 < (size (invariant_factors A)))%N. by rewrite lt0n size_eq0 nnil_inv_factors. rewrite (big_nth 0) big_mkord (bigD1 (Ordinal H0)) //. rewrite size_map -lt0n addn_gt0 lt0n size_eq0. apply/orP; left; apply/eqP=>/undup_nil; apply/eqP. rewrite -root_seq_nil -ltnNge. have:= (mem_nth 0 H0). by rewrite mem_filter; case/andP=> ->. move=> i; rewrite size_map size_enum_ord=> Hi. rewrite (nth_map 0) ?size_enum_ord //. by rewrite (nth_ord_enum 0 (Ordinal Hi)) !mxE eqxx. 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) CoqEAL(frobenius_form)