proposition: Lemma eigen_diag n (A : 'M_n.+1) : let sp := root_seq_poly (invariant_factors A) in let sizes := [seq (x.2).-1 | x <- sp] in perm_eq [seq (Jordan_form A) i i | i <- enum 'I_(size_sum sizes).+1] (root_seq (char_poly A)).
proof: Proof. have Hinj: injective (fun (c : R) => 'X - c%:P). by move=> x y /= H; apply/polyC_inj/oppr_inj/(addrI 'X). apply: (perm_map_inj Hinj). apply: (@unicity_decomposition _ _ _ (char_poly A)). + move=> r /(nthP 0) []i; rewrite !size_map=> Hi. rewrite (nth_map 0) ?size_map // => <-. exact: irredp_XsubC. - move=> r /(nthP 0) []i; rewrite !size_map=> Hi. rewrite (nth_map 0) ?size_map // => <-. exact: irredp_XsubC. + move=> r /(nthP 0) []i; rewrite !size_map=> Hi. rewrite (nth_map 0) ?size_map // => <-. exact: monicXsubC. - move=> r /(nthP 0) []i; rewrite !size_map=> Hi. rewrite (nth_map 0) ?size_map // => <-. exact: monicXsubC. + by rewrite !big_map; exact: Jordan_char_poly. rewrite big_map {1}[char_poly A]root_seq_eq. by rewrite (monicP (char_poly_monic A)) scale1r. 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)