definition of simple group

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Jan 15, 2025 · a4a574f · a4a574f
1 parent ef81e30
commit a4a574f
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 *)