From 216bc703af76c91e884cfca904491bd6ec7714a9 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 3 Jan 2025 21:07:31 +0000 Subject: [PATCH] fix notations in subgroup lemmas Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index 0cf0c2a828..904fa33f3a 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -122,9 +122,9 @@ Defined. Section SubgroupElements. Context {G : Group} (H : Subgroup G) (x y : G). - Definition subgroup_in_unit : H mon_unit := issubgroup_in_unit. - Definition subgroup_in_inv : H x -> H (- x) := issubgroup_in_inv x. - Definition subgroup_in_inv' : H (- x) -> H x := issubgroup_in_inv' x. + Definition subgroup_in_unit : H 1 := issubgroup_in_unit. + Definition subgroup_in_inv : H x -> H x^ := issubgroup_in_inv x. + Definition subgroup_in_inv' : H x^ -> H x := issubgroup_in_inv' x. Definition subgroup_in_op : H x -> H y -> H (x * y) := issubgroup_in_op x y. Definition subgroup_in_op_inv : H x -> H y -> H (x * y^) := issubgroup_in_op_inv x y. Definition subgroup_in_inv_op : H x -> H y -> H (x^ * y) := issubgroup_in_inv_op x y.