proposition: Lemma det_diag_mx_seq m (s : seq R) : size s = m -> \det (diag_mx_seq m m s) = \prod_(i <- s) i.
proof: Proof. by move=> <-; rewrite det_diag_mx_seq_truncated take_size // leqnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm poly mxpoly finfun tuple) mathcomp(matrix bigop zmodp polydiv) ssrcomplements dvdring