proposition: Lemma det_triangular_mx : forall n (M : 'M[R]_n), upper_triangular_mx M -> \det M = \prod_i M i i.
proof: Proof. elim=> [M _|n IHn]; first by rewrite det_mx00 big_ord0. rewrite -[n.+1]add1n=> M. rewrite -(submxK M)=> HM. rewrite (upper_triangular_block_mxdl HM) // det_ublock IHn. rewrite {1}[ulsubmx M]mx11_scalar det_scalar1 big_split_ord big_ord1. by rewrite block_mxEul; congr *%R; apply:eq_bigr=> i _; rewrite block_mxEdr. exact: (upper_triangular_block_mxdr HM). 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