From 0c86242758cc7caa7233da2c62a0f6d5f0ae3ad4 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 2 Jan 2025 15:43:16 +0000 Subject: [PATCH] trivial and maximal subgroup are normal subgroups Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index 84a692b804..3cfe749ce0 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -423,6 +423,22 @@ Proof. by snrapply Build_IsNormalSubgroup'. Defined. +(** The trivial subgroup is a normal subgroup. *) +Global Instance isnormal_trivial_subgroup {G : Group} + : IsNormalSubgroup (trivial_subgroup G). +Proof. + intros x y p; cbn in p |- *. + apply grp_moveL_1V in p. + by apply grp_moveL_V1. +Defined. + +(** The maximal subgroup (the group itself) is a normal subgroup. *) +Global Instance isnormal_maximal_subgroup {G : Group} + : IsNormalSubgroup (maximal_subgroup G). +Proof. + intros x y p; exact tt. +Defined. + (** Left and right cosets are equivalent in normal subgroups. *) Definition equiv_in_cosetL_in_cosetR_normalsubgroup {G : Group} (N : NormalSubgroup G) (x y : G)