Merge pull request #2196 from Alizter/ps/rr/definition_of_simple_group

definition of simple group
HoTT · Jan 15, 2025 · 234ede0 · 234ede0
2 parents ef81e30 + a4a574f
commit 234ede0
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
@@ -610,6 +610,12 @@ Proof.
   split; by apply subgroup_in_op_inv.
 Defined.
 
+(** *** Simple groups *)
+
+Class IsSimpleGroup (G : Group)
+  := is_simple_group : forall (N : Subgroup G) `{IsNormalSubgroup G N},
+    IsTrivialGroup N + IsMaximalSubgroup N.
+
 (** *** The subgroup generated by a subset *)
 
 (** Underlying type family of a subgroup generated by subset *)