proposition: Lemma kernelP (M N : {fpmod R}) (phi : 'Mor(M,N)) : is_kernel phi (kernel phi).
proof: Proof. split; first by rewrite mulkmor. move=> L X; apply: (iffP idP) => [|[Y]]; last first. move/eqmorMr/eqmor_ltrans <-; rewrite -mulmorA. by rewrite (eqmor_ltrans (eqmorMl _ (mulkmor _))) mulmor0. rewrite /eqmor; rewrite subr0 -dvd_ker => /dvdmxP [Y Yeq]. have Ymor : pres (source (kernel phi)) %| pres L *m Y. by rewrite /= dvd_ker -mulmxA -Yeq dvdmx_morphism. by exists (Morphism Ymor); rewrite Yeq subrr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice matrix bigop zmodp mxalgebra poly) ssrcomplements stronglydiscrete coherent edr