proposition: Lemma lker0P f : reflect (injective f) (lker f == 0%VS).
proof: Proof. rewrite -subv0; apply: (iffP subvP) => [injf u v eq_fuv | injf u]. apply/eqP; rewrite -subr_eq0 -memv0 injf //. by rewrite memv_ker linearB /= eq_fuv subrr. by rewrite memv_ker memv0 -(inj_eq injf) linear0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)