From ad43e040880af40f62f0fb724037e5dda9fe33cc Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 4 Jan 2025 17:44:41 +0000 Subject: [PATCH] address review comments Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index a2cc95d58c..0878378979 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -496,9 +496,8 @@ Proof. Defined. (** The property of being the trivial group is useful. Note that any group can be automatically coerced to its maximal subgroup, so it makes sense for this predicate to be applied to groups in general. *) -Definition IsTrivialGroup@{i} {G : Group@{i}} (H : Subgroup@{i i} G) := - forall x, H x -> trivial_subgroup G x. -Existing Class IsTrivialGroup. +Class IsTrivialGroup@{i} {G : Group@{i}} (H : Subgroup@{i i} G) := + istrivialgroup : forall x, H x -> trivial_subgroup G x. Global Instance istrivial_trivial_subgroup {G : Group} : IsTrivialGroup (trivial_subgroup G) @@ -506,7 +505,8 @@ Global Instance istrivial_trivial_subgroup {G : Group} (** Trivial groups are isomorphic to the trivial group. *) Definition istrivial_iff_grp_iso_trivial_subgroup {G : Group} (H : Subgroup G) - : IsTrivialGroup H <-> (H : Group) $<~> trivial_subgroup G. + : IsTrivialGroup H + <-> (subgroup_group H $<~> subgroup_group (trivial_subgroup G)). Proof. split. - intros T.