子群与子群判定

Introduction

一个群的子集 H ⊆ G 称为**子群 (Subgroup)**，如果它本身也是一个群（关于 G 中的同样运算）。要检查 H 是否是子群，通常只需验证三条： 1. **包含单位元**：`1 ∈ H` 2. **封闭于乘法**：若 `a, b ∈ H`，则 `a * b ∈ H` 3. **封闭于逆元**：若 `a ∈ H`，则 `a⁻¹ ∈ H` 本关目标：两个子群的**交集仍是子群**。即：如果 H₁ 和 H₂ 都是子群，那么 H₁ ∩ H₂ 也是子群。这是子群论的基础构造——它保证了子群族有「最小的」子群。

本关学到的新东西

策略 (Tactics)

refine ⟨?_, ?_⟩把包含多个部分的目标拆分成若干子目标，用 `?_` 占位

概念 (Concepts)

子群 (Subgroup)群的子集，自身在该运算下也是群

子群判定条件包含单位元 + 乘法封闭 + 逆元封闭

IsSubgroup用 Set α 和命题定义的子群谓词

证明目标

当前目标

G : Type

H₁ H₂ : Set G

mul : G → G → G

one : G

inv : G → G

h₁ : IsSubgroup H₁

h₂ : IsSubgroup H₂

⊢IsSubgroup (H₁ ∩ H₂)

分步提示

1.现在目标是证明交集的三个条件（即 `IsSubgroup (H₁ ∩ H₂)` 展开后的形式）。第一个条件：`one ∈ H₁ ∩ H₂`。
2.`one ∈ H₁ ∩ H₂` 展开就是 `one ∈ H₁ ∧ one ∈ H₂`。用 `constructor` 拆开，然后分别从 `h₁.left` 和 `h₂.left` 获取 h₁ 和 h₂ 各自的单位元条件。
3.第二个条件：对任意 a b，如果它们在交集中，它们的乘积也在交集中。`rcases` 拆开 a b 在交集中的条件（各是两个命题的 ∧），然后再次用构造子。乘法封闭性分别从 h₁ 和 h₂ 各自的封闭性得到。
4.第三个条件类似：对任意 a 在交集中，a⁻¹ 也在交集中。拆开 a 的条件，分别用 h₁ 和 h₂ 的逆封闭性。

怎么玩：编辑器里有预写代码。直接点 运行 ▶ 看效果，或修改代码后运行。卡住了看左侧的提示。

Lean 代码编辑器