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) ❙
❚