群的定义与基本性质

Introduction

群 (Group) 是现代代数的基石。一个群由一个集合 G 和一个二元运算 `*` 组成，满足三条公理： 1. **结合律**：`(a * b) * c = a * (b * c)` 2. **单位元**：存在 `1`，使得 `1 * a = a` 且 `a * 1 = a` 3. **逆元**：每个元素 `a` 有逆 `a⁻¹`，使得 `a⁻¹ * a = 1` 且 `a * a⁻¹ = 1` 本关目标：证明 `a⁻¹ * (a * b) = b`——这体现了「逆元的本质就是撤销操作」。我们会在课程中**手动定义**群的结构（用 `variable` + `notation`），这样你能真正理解每个公理是如何被使用的。

本关学到的新东西

策略 (Tactics)

calc链式等式证明块。`calc a = b := by ... _ = c := by ...`

rw [← ...]反向重写。`rw [← mul_assoc]` 把 a*(b*c) 变成 (a*b)*c

概念 (Concepts)

群 (Group)集合 + 满足结合律/单位元/逆元的二元运算

notation自定义符号。`notation a * b => mul a b` 让代码像数学

calc 块逐步等式推导，每行列出一个等式和它的证明理由

证明目标

当前目标

G : Type

mul : G → G → G

one : G

inv : G → G

mul_assoc : ∀ a b c : G, (a * b) * c = a * (b * c)

one_mul : ∀ a : G, 1 * a = a

mul_one : ∀ a : G, a * 1 = a

mul_inv_left : ∀ a : G, a⁻¹ * a = 1

⊢a⁻¹ * (a * b) = b

分步提示

1.用 `calc` 块来做等式链式推导。从左边 `a⁻¹ * (a * b)` 开始。
2.第一步，用结合律把括号重新分组：`rw [mul_assoc]` 或 `rw [← mul_assoc]`。`a⁻¹ * (a * b)` 中括号在右边，用 `rw [← mul_assoc (inv a) a b]` 变成 `(a⁻¹ * a) * b`。
3.现在 `(a⁻¹ * a) * b`。用 `rw [mul_inv_left a]` 把 `a⁻¹ * a` 替换为 `1`，得到 `1 * b`。
4.最后 `rw [one_mul b]`，`1 * b` 变成 `b`。完成！
5.calc 的语法：calc 后面每一行是 `expr = expr := by ...`，可以用 rw 也可以用 simp 等。最后一行 `_ = b := by rw [one_mul]`。

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

Lean 代码编辑器