proposition: Lemma kermxP m n (M : 'M[R]_(m,n)) (X : 'rV_m) : reflect (exists Y : 'rV_m, X = Y *m kermx M) (X *m M == 0).
proof: Proof. apply: (iffP eqP)=> [|[Y ->]]; last by rewrite -mulmxA mul_kermx mulmx0. by move/mulmxKV_kermx=> hX; exists (X *m col_ebase M). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path tuple) mathcomp(perm fingroup choice ssralg fintype finfun poly polydiv) mathcomp(bigop matrix zmodp mxalgebra) ssrcomplements dvdring mxstructure similar minor binetcauchy stronglydiscrete coherent