proposition: Fact ker_sub_ahom_is_aspace (f g : ahom aT rT) : is_aspace (lker (ahval f - ahval g)).
proof: Proof. rewrite /is_aspace has_algid1; last by apply/eqlfunP; rewrite !rmorph1. apply/prodvP=> a b /eqlfunP Dfa /eqlfunP Dfb. by apply/eqlfunP; rewrite !rmorphM /= Dfa Dfb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)