fact: Structure iso_map := IsoMap { apply : object_map; _ : group_valued apply; _ : closed apply; _ : iso_continuous apply }.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)