proposition: Lemma Smith_companion (p : E) : (1 < size p)%N -> p \is monic -> equivalent (Smith_form (char_poly_mx (companion_mx p))) (diag_mx_seq (size p).-2.+1 (size p).-2.+1 (rcons (nseq (size p).-2 1) p)).
proof: Proof. move=> Hsp Hmp. rewrite /Smith_form -diag_mx_seq_takel. set s := take _ _. have Hs1: (size p).-2.+1 = size s. by rewrite -(size_Frobenius_seq (companion_mx p)) size_map. have Hs2: (size p).-2.+1 = size (rcons (nseq (size p).-2 1) p). by rewrite size_rcons size_nseq. apply: eqd_equiv=> //; first by rewrite -Hs1 -Hs2. have := leqnSn (size p).-2. rewrite -[X in (_ <= X)%N]minnn=> Hop. have Hsort: sorted %|%R s. by apply/(sorted_take (@dvdr_trans _))/sorted_Smith. have := (equiv_Smith (char_poly_mx (companion_mx p))). rewrite /Smith_form -diag_mx_seq_takel=> Hsm. have {Hop Hsort Hsm} := (Smith_gcdr_spec Hop Hsort Hsm). 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 ord0)). apply: big_gcdr_def; exists (finfun (lift ord_max)). rewrite /minor.minor /minor.submatrix /=. set M := \matrix_(_,_) _. have Hut: upper_triangular_mx M. apply/upper_triangular_mxP => i j Hij. rewrite !mxE !ffunE -(inj_eq (@ord_inj _)) lift0 lift_max. rewrite !eqn_leq !(leqNgt _ j) ltn_ord subr0. by rewrite ltnW // ltnNge Hij !andFb subr0. rewrite (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 (leqNgt _ i) ltn_ord sub0r subr0. by apply/dvdrP; exists ((-1)^+ (size p).-2); rewrite -expr2 sqrr_sign. have Hip: s`_(size p).-2 %= p. rewrite eqd_sym in Hd1. rewrite -(mul1r s`_(size p).-2) (eqd_ltrans (eqd_mulr _ Hd1)). rewrite -{2}(comp_char_polyK Hmp Hsp) /char_poly -det_Smith. rewrite /Smith_form -diag_mx_seq_takel. rewrite det_diag_mx_seq // eqd_sym (big_nth 0) big_mkord. by rewrite -Hs1 big_ord_recr /=. move/eqd_big_mul1: Hd1 => H i. case: (ltngtP i (size p).-2) => 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 eqxx ltnn. 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)