proposition: Lemma mx_trace0 : forall n, \tr ('0m : 'M_n) === 0.
proof: Proof. by move=> n; apply (big1 (I:=ordinal_finType n))=> i _; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms