proposition: Fact centraliser1_is_aspace u : is_aspace 'C[u].
proof: Proof. rewrite /is_aspace has_algid1 ?cent1v1 //=. apply/prodvP=> v w /cent1vP-cuv /cent1vP-cuw. by apply/cent1vP; rewrite -mulrA cuw !mulrA cuv. 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)