proposition: Fact iso_kernel_eq0 (phi : 'Iso(M,N)) : kernel phi %= 0.
proof: Proof. by case: phi => /= ? /andP[]. 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