proposition: Lemma algid_center A : algid 'Z(A) = algid A.
proof: Proof. rewrite -(algidl (subvP (centerv_sub A) _ (memv_algid _))) algidr //=. by rewrite memv_cap memv_algid centv_algid. 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)