From a4a574fa8a6bccd3d4f4a0ec77436815df4c5f58 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Thu, 2 Jan 2025 15:56:05 +0000
Subject: [PATCH] definition of simple group

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: 478c8d63-658b-40d7-a890-b45cc6120c7f -->
---
 theories/Algebra/Groups/Subgroup.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 0ebeb032cc..b5356e5bef 100644
--- 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 *)