群的更多性质

Introduction

掌握了群的基本公理后，我们来探索群的一些重要导出性质。本关证明两个经典结论： 1. **左右消去律**：如果 `a * b = a * c`，那么 `b = c`（左边同乘同一个元素可以消去） 2. **逆元的平方**：`(a⁻¹)⁻¹ = a` 这些性质从公理出发都可以严格证明——而且和中学代数里的推导很像！

本关学到的新东西

概念 (Concepts)

消去律若 a*b = a*c 则 b = c。从群公理可导出

等式变换技巧插单位元、插逆元对、重结合——群论证明的核心手法

证明目标

当前目标

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 * b = a * c → b = c

分步提示

1.假设 `a * b = a * c`，要证明 `b = c`。关键思路：在等式两边同时左乘 `a⁻¹`。
2.用 `intro h` 引入前提。`h` 是 `a * b = a * c`。
3.从 `h` 出发，两边同时左乘 `a⁻¹`：用 `calc` 块或者 `rw` 链。
4.具体做法：`calc b = 1 * b := by rw [one_mul] ...`，或者 `have h' : a⁻¹ * (a * b) = a⁻¹ * (a * c) := by rw [h]`。
5.然后用 `rw [← mul_assoc, mul_inv_left, one_mul]` 化简左边为 `b`，同理右边得 `c`。最终得到 `b = c`。

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

Lean 代码编辑器