proposition: Lemma injm_cent1 x : x \in D -> f @* 'C[x] = 'C_(f @* D)[f x].
proof: Proof. by move=> Dx; rewrite injm_norm ?morphim_set1 ?sub1set. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)