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 ❚

theory StabilizerChain : fnd:?Logic =
	include ?PermutationGroups ❙
	include ?GroupActions ❙
	
	/T A step in a Schreier-Sims Stabiliser Chain ❙
	// step : {Ω : type} {G : group} {act : rightGroupActions G Ω} ⟶ 
		{' basept : Ω, orbit : rorbit act basept, stabiliser : rstab act β '} ❙

	
	
❚