proposition: Lemma lkerE f U : (U <= lker f)%VS = (f @: U == 0)%VS.
proof: Proof. rewrite unlock -dimv_eq0 /dimv /subsetv !genmxE mxrank_eq0. by rewrite (sameP sub_kermxP eqP). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)