proposition: Lemma col_id_mulmx m n (M : 'M[R]_(m,n)) i : M *m col i 1%:M = col i M.
proof: Proof. apply/matrixP=> k l; rewrite !mxE. rewrite (bigD1 i) // big1 /= ?addr0 ?mxE ?eqxx ?mulr1 // => j /negbTE neqji. by rewrite !mxE neqji mulr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype finfun perm matrix bigop zmodp mxalgebra) mathcomp(choice poly polydiv mxpoly binomial)