Skip to content

Update S01_Groups.lean #31

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Update S01_Groups.lean #31

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 2 additions & 3 deletions MIL/C09_Groups_and_Rings/S01_Groups.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -570,7 +570,6 @@ def CayleyIsoMorphism (G : Type*) [Group G] : G ≃* (toPermHom G G).range :=
-- QUOTE.

/- TEXT:
以下是这段话的翻译：

请注意，在上述定义之前，并不需要一定是群，而是可以是幺半群或者任何具有乘法操作的类型。

Expand All @@ -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.

Expand Down Expand Up @@ -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]
Expand Down