proposition: Fact centraliser_is_aspace V : is_aspace 'C(V).
proof: Proof. rewrite /is_aspace has_algid1 ?centv1 //=. apply/prodvP=> u w /centvP-cVu /centvP-cVw. by apply/centvP=> v Vv; rewrite /= -mulrA cVw // !mulrA cVu. 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)