环的定义与基本性质

Introduction

环 (Ring) 是比群更丰富的代数结构——它有两个运算：加法和乘法。一个环 R 满足： - **加法群**：`(R, +, 0, -)` 是交换群（即 Abelian group） - **乘法半群**：`(R, *)` 满足结合律，有单位元 1 - **分配律**：`a * (b + c) = a*b + a*c` 和 `(a + b) * c = a*c + b*c` 本关目标：证明环中最基本的性质——**零乘任何元素得零**：`0 * a = 0`。你会看到，分配律在环论证明中扮演核心角色。

本关学到的新东西

概念 (Concepts)

环 (Ring)集合 + 加法构成交换群 + 乘法满足结合律/分配律

分配律a*(b+c) = a*b + a*c。连接加法和乘法的桥梁

加法零元 (0)a + 0 = a。在环论中和乘法零元是同一个 0

证明目标

当前目标

R : Type

add mul : R → R → R

zero one : R

neg : R → R

add_assoc : ∀ a b c, (a + b) + c = a + (b + c)

add_comm : ∀ a b, a + b = b + a

add_zero : ∀ a, a + 0 = a

add_neg : ∀ a, a + (-a) = 0

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

one_mul : ∀ a, 1 * a = a

mul_one : ∀ a, a * 1 = a

left_distrib : ∀ a b c, a * (b + c) = a * b + a * c

right_distrib : ∀ a b c, (a + b) * c = a * c + b * c

⊢0 * a = 0

分步提示

1.关键技巧：把 `0` 写成 `0 + 0`，然后利用分配律。`0 = 0 + 0` 由 `add_zero 0` 给出。
2.`calc 0 * a = (0 + 0) * a := by rw [add_zero 0]` 把左边展开。
3.然后 `(0 + 0) * a = 0 * a + 0 * a`，这来自 `right_distrib 0 0 a`。
4.现在我们得到 `0 * a = 0 * a + 0 * a`。像群论中一样，两边同时加 `-(0*a)` 消去。
5.`calc 0 = (0 * a) + (-(0 * a)) := by rw [add_neg] ...` 把结果串联起来。最终得到 `0 * a = 0`。

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

Lean 代码编辑器