From 7c9943ecc2ef50c72e7334e18187501bb875c50b Mon Sep 17 00:00:00 2001
From: Meowrium <128562807+Meowrium@users.noreply.github.com>
Date: Fri, 4 Jul 2025 18:04:42 +0800
Subject: [PATCH] Update S01_Groups.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

语言调整
---
 MIL/C09_Groups_and_Rings/S01_Groups.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/MIL/C09_Groups_and_Rings/S01_Groups.lean b/MIL/C09_Groups_and_Rings/S01_Groups.lean
index cc12329c..ec93d809 100644
--- a/MIL/C09_Groups_and_Rings/S01_Groups.lean
+++ b/MIL/C09_Groups_and_Rings/S01_Groups.lean
@@ -570,7 +570,6 @@ def CayleyIsoMorphism (G : Type*) [Group G] : G ≃* (toPermHom G G).range :=
 -- QUOTE.
 
 /- TEXT:
-以下是这段话的翻译：
 
 请注意，在上述定义之前，并不需要一定是群，而是可以是幺半群或者任何具有乘法操作的类型。
 
@@ -596,7 +595,7 @@ example {G X : Type*} [Group G] [MulAction G X] : Setoid X := orbitRel G X
 EXAMPLES: -/
 -- QUOTE:
 example {G X : Type*} [Group G] [MulAction G X] :
-    X ≃ (ω : orbitRel.Quotient G X) × (orbit G (Quotient.out' ω)) :=
+    X ≃ (ω : orbitRel.Quotient G X) × (orbit G (Quotient.out ω)) :=
   MulAction.selfEquivSigmaOrbits G X
 -- QUOTE.
 
@@ -721,7 +720,7 @@ example {G G': Type*} [Group G] [Group G']
 -- QUOTE.
 
 /- TEXT:
-需要注意的一个细微点是，类型 ``G ⧸ N`` 实际上依赖于 ``N``（在定义等同的范围内），因此证明两个正规子群 ``N`` 和 ``M`` 是相等的并不足以使相应的商群相等。然而，在这种情况下，整体性质确实给出了一个同构。
+需要注意的一个细微点是，类型 ``G ⧸ N`` 实际上依赖于 ``N`` （在定义等同的范围内），因此证明两个正规子群 ``N`` 和 ``M`` 是相等的并不足以使相应的商群相等。然而，在这种情况下，整体性质确实给出了一个同构。
 EXAMPLES: -/
 -- QUOTE:
 example {G : Type*} [Group G] {M N : Subgroup G} [M.Normal]