proposition: Lemma injm_abelian A : A \subset D -> abelian (f @* A) = abelian A.
proof: Proof. by move=> sAD; rewrite /abelian -subsetIidl -injm_subcent // injmSK ?subsetIidl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)