proposition: Lemma char_poly_triangular_mx n (M : 'M[R]_n) : upper_triangular_mx M -> char_poly M = \prod_i ('X - (M i i)%:P).
proof: Proof. move=> Ht; rewrite /char_poly det_triangular_mx ?char_poly_mx_triangular_mx //. by apply: eq_bigr=> i _; rewrite !mxE eqxx. 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