Commit 2ae47da9 authored by Michael Kohlhase's avatar Michael Kohlhase

two definitions

parent 7a95070d
......@@ -137,8 +137,7 @@ theory Group : base:?Logic =
automorphisms : group ⟶ ℕ ❙
cyclic : group ⟶ prop ❙
degree : group ⟶ ℕ ❙
order : group ⟶ ℕ ❙
order : group ⟶ ℕ ❘ = [g] cardinality (baseset g)❙
parity : group ⟶ ℤ ❙
solvable : group ⟶ prop ❙
psolvable : group ⟶ ℕ+ ⟶ prop ❙
......
......@@ -13,6 +13,9 @@ theory PermutationGroups =
permutationGroup : {Ω : type} subgroupOf (symmetricGroup Ω) ❘ # permutationGroup 1 ❙
// permutationGroupByGenerators : {Ω : type} subtypeOf (symmetricGroup Ω) ⟶ permutationGroup Ω ❙
degree : permutationGroup ⟶ ℕ ❘ = [g] cardinality g❙
theory PermutationGroupsN =
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment