proposition: Lemma similar_cj n (lam : R) : similar (companion_mx (('X - lam%:P)^+ n.+1)) (Jordan_block lam n.+1).
proof: Proof. set p := _^+n.+1. have Hmp: p \is monic by rewrite monic_exp // monicXsubC. have Hsp: (1 < size p)%N by rewrite size_exp_XsubC. apply/similar_fundamental. apply: (equiv_trans (equiv_Smith _)). apply: (equiv_trans (Smith_companion Hsp Hmp)). set M := char_poly_mx _. apply/equiv_sym/(equiv_trans (equiv_Smith M)). rewrite /Smith_form -diag_mx_seq_takel. set s := take _ _. have Hs1: size s = n.+1. rewrite size_Smith_seq // -/(char_poly _) char_poly_Jordan_block. by rewrite -size_poly_eq0 size_exp_XsubC. apply: eqd_equiv; rewrite ?size_exp_XsubC // ?size_rcons ?size_nseq //=. have Hsort: sorted (@dvdr _) s. by apply/(sorted_take (@dvdr_trans _))/sorted_Smith. move: (equiv_Smith M). rewrite /Smith_form -diag_mx_seq_takel => Hequiv. have Hlemin: (n <= minn n.+1 n.+1)%N by rewrite minnn. move: (Smith_gcdr_spec Hlemin Hsort Hequiv). set d := \big[_/_]_(_<_) _=> H. have {H} Hd1: d %= 1. apply/(eqd_trans H)/andP; split; last by rewrite dvd1r. apply: big_gcdr_def; exists (finfun (lift ord_max)). apply: big_gcdr_def; exists (finfun (lift ord0)). rewrite /minor.minor /minor.submatrix /=. set N := \matrix_(_,_) _. have Hut: upper_triangular_mx N^T. apply/upper_triangular_mxP=> i j Hij. rewrite !mxE !ffunE -(inj_eq (@ord_inj _)) lift0 lift_max. rewrite !eqn_leq !(leqNgt _ j) ltnS (ltnW Hij) ltnNge Hij. by rewrite andbF addr0 subr0. rewrite -det_tr (det_triangular_mx Hut). rewrite (eq_bigr (fun _ => -1)) ?prodr_const ?card_ord; last first. move=> i; rewrite !mxE !ffunE -(inj_eq (@ord_inj _)) lift0 lift_max. by rewrite eqxx !eqn_leq ltnn andbF sub0r add0r. by apply/dvdrP; exists ((-1)^+ n); rewrite -expr2 sqrr_sign. have Hip: s`_n %= p. rewrite eqd_sym in Hd1. rewrite -(mul1r s`_n) (eqd_ltrans (eqd_mulr _ Hd1)). rewrite /p -char_poly_Jordan_block /char_poly -det_Smith. rewrite /Smith_form -diag_mx_seq_takel det_diag_mx_seq //. by rewrite (big_nth 0) big_mkord Hs1 big_ord_recr. move/eqd_big_mul1: Hd1 => H i. case: (ltngtP i n) => Hi. - by rewrite nth_rcons size_nseq Hi nth_nseq Hi (H (Ordinal Hi)). - by rewrite !nth_default // ?Hs1 // size_rcons size_nseq. by rewrite nth_rcons size_nseq Hi ltnn eqxx. 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)