Subgroup/QuotientGroup: minor fixes

HoTT · Jan 21, 2025 · 98ce5f0 · 98ce5f0
1 parent b2c7d9f
commit 98ce5f0
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 5 deletions.
diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
@@ -124,11 +124,10 @@ Section Cosets.
     nrapply finite_quotient.
     1-5: exact _.
     intros x y.
-    pose (dec_H := detachable_finite_subset H).
-    apply dec_H.
+    apply (detachable_finite_subset H).
   Defined.
 
-  (** The index of a subgroup is the number of possible cosets of the subgroup. *) 
+  (** The index of a subgroup is the number of cosets of the subgroup. *)
   Definition subgroup_index `{Univalence, Finite G, Finite H} : nat
     := fcard LeftCoset.
 

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
@@ -392,8 +392,6 @@ Proof.
     apply equiv_subgroup_op_inv.
 Defined.
 
-(** The sigma type of any two right cosets are equivalent. *)
-
 (** A normal subgroup is a subgroup closed under conjugation. *)
 Class IsNormalSubgroup {G : Group} (N : Subgroup G)
   := isnormal : forall {x y}, N (x * y) -> N (y * x).