From 087a459e7f6d49e20b2d90665cfc89404c2d5f26 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 2 Jan 2025 15:37:23 +0000 Subject: [PATCH] complete and organise grp_moveL_1M type lemmas Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Group.v | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v index 4a6a5d70bd..26cedd99f1 100644 --- a/theories/Algebra/Groups/Group.v +++ b/theories/Algebra/Groups/Group.v @@ -508,20 +508,29 @@ Section GroupMovement. (** *** Moving elements equal to unit. *) - Definition grp_moveL_1M : x * y^ = mon_unit <~> x = y + Definition grp_moveL_1M : x * y^ = 1 <~> x = y := equiv_concat_r (grp_unit_l _) _ oE grp_moveL_gM. - Definition grp_moveL_1V : x * y = mon_unit <~> x = y^ - := equiv_concat_r (grp_unit_l _) _ oE grp_moveL_gV. - - Definition grp_moveL_M1 : y^ * x = mon_unit <~> x = y + Definition grp_moveL_M1 : y^ * x = 1 <~> x = y := equiv_concat_r (grp_unit_r _) _ oE grp_moveL_Mg. + + Definition grp_moveL_1V : x * y = 1 <~> x = y^ + := equiv_concat_r (grp_unit_l _) _ oE grp_moveL_gV. + + Definition grp_moveL_V1 : y * x = 1 <~> x = y^ + := equiv_concat_r (grp_unit_r _) _ oE grp_moveL_Vg. - Definition grp_moveR_1M : mon_unit = y * x^ <~> x = y - := (equiv_concat_l (grp_unit_l _) _)^-1%equiv oE grp_moveR_gM. + Definition grp_moveR_1M : 1 = y * x^ <~> x = y + := (equiv_concat_l (grp_unit_l _) _)^-1 oE grp_moveR_gM. + + Definition grp_moveR_M1 : 1 = x^ * y <~> x = y + := (equiv_concat_l (grp_unit_r _) _)^-1 oE grp_moveR_Mg. + + Definition grp_moveR_1V : 1 = y * x <~> x^ = y + := (equiv_concat_l (grp_unit_l _) _)^-1 oE grp_moveR_gV. - Definition grp_moveR_M1 : mon_unit = x^ * y <~> x = y - := (equiv_concat_l (grp_unit_r _) _)^-1%equiv oE grp_moveR_Mg. + Definition grp_moveR_V1 : mon_unit = x * y <~> x^ = y + := (equiv_concat_l (grp_unit_r _) _)^-1 oE grp_moveR_Vg. (** *** Cancelling elements equal to unit. *)