proposition: Lemma char_poly_trig {R : comRingType} n (A : 'M[R]_n) : is_trig_mx A -> char_poly A = \prod_(i < n) ('X - (A i i)%:P).
proof: Proof. move=> /is_trig_mxP Atrig; rewrite /char_poly det_trig. by apply: eq_bigr => i; rewrite !mxE eqxx. by apply/is_trig_mxP => i j lt_ij; rewrite !mxE -val_eqE ltn_eqF ?Atrig ?subrr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)