proposition: Lemma mulmx_diag_mx m n (M : 'M_(m, n)) : diag_mx M = invmx (col_ebase M) *m M *m invmx (row_ebase M).
proof: Proof. rewrite /col_ebase /diag_mx /row_ebase /diag /smith_seq !invmxK. case: smithP=> L0 d R0 h1 h2 _ _. rewrite diag_mx_seq_filter0. by rewrite diag_mx_seq_take_min. exact: (sorted_take (@dvdr_trans [dvdRingType of R])). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path tuple) mathcomp(perm fingroup choice ssralg fintype finfun poly polydiv) mathcomp(bigop matrix zmodp mxalgebra) ssrcomplements dvdring mxstructure similar minor binetcauchy stronglydiscrete coherent