namespace http://mathhub.info/MitM/core/algebra/groups 
import fnd http://mathhub.info/MitM/Foundation 
import core http://mathhub.info/MitM/core 


/T This obviously doesn't type check yet ❙
theory ActionOnPolynomials : fnd:?Logic = 
	include ?SymmetricGroup
	include ?GroupAction
	
	/T I think this is what I would want
	   though it is entirely unclear to me right now
	   how one would encode an induced action (if at all)❙	
  symmetricGroupActionOnPolynomials : type = {vars : type} rightGroupActions (SymmetricGroup vars) (Polynomials vars) ❙
  groupActionOnPolynomials : type = {vars : type} {act : rightGroupActions G vars} rightGroupActions G (Polynomials vars) ❙