proposition: Lemma prod_minor_seq : \prod_(i < k) s`_i = minor [ffun x : 'I_k => widen_minl (widen_ord Hk x)] [ffun x : 'I_k => widen_minr (widen_ord Hk x)] (diag_mx_seq m n s).
proof: Proof. rewrite /minor /submatrix. elim: k Hk=>[H|j /= IHj Hj]; first by rewrite det_mx00 big_ord0. have IH : j <= (minn m n) by apply: ltnW. apply: esym; rewrite (expand_det_row _ ord_max) big_ord_recr /=. rewrite big1 ?add0r /cofactor=> [|i _]; last first. by rewrite !mxE !ffunE eqn_leq leqNgt (ltn_ord i) andFb mul0r. rewrite !mxE !ffunE eqxx exprD -expr2 sqrr_sign mul1r. rewrite /row' /col'; set M := matrix_of_fun _ _. rewrite big_ord_recr /= (IHj IH) mulr1n mulrC; do 2!f_equal. apply/matrixP=> i l; rewrite !mxE !ffunE /= /bump. by do 2!rewrite leqNgt (ltn_ord _) add0n. 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