namespace http://mathhub.info/MitM/core/algebra/groups 

import fnd http://mathhub.info/MitM/Foundation 
import sets http://mathhub.info/MitM/core/sets 
import arith http://mathhub.info/MitM/core/arithmetics 


/T Permutation groups are subgroups of SymmetricGroup(Ω) ❚
theory PermutationGroups =
	include ?Subgroups 
	include ?SymmetricGroup 
	

	permutationGroup : {Ω : type} subgroupOf (symmetricGroup Ω)  # permutationGroup 1 
	// permutationGroupByGenerators : {Ω : type} subtypeOf (symmetricGroup Ω) ⟶ permutationGroup Ω ❙
	
	degree : permutationGroup ⟶ ℕ  = [g] cardinality g



theory PermutationGroupsN =
	include ?Subgroups 
	include ?SymmetricGroup 
	include ?SymmetricGroupOfN 

  permutationGroup : {Ω : type} subgroupOf (symmetricGroup Ω) 
  // permutationGroupByGenerators : {Ω : type} subtypeOf (symmetricGroup Ω) ⟶ permutationGroup Ω ❙