proposition: Lemma restr_isom (A : {group aT}) (R : {group rT}) (sAG : A \subset G) : isom G R f -> isom A (f @* A) (restrm sAG f).
proof: Proof. exact: restr_isom_to. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)