proposition: Lemma colE m n (i : 'I_n) (M : 'M[R]_(m, n)) : col i M = M *m delta_mx i 0.
proof: Proof. by apply/trmx_inj; rewrite trmx_mul trmx_delta -rowE tr_col. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice matrix bigop zmodp mxalgebra poly) ssrcomplements dvdring stronglydiscrete