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