环的更多性质

Introduction

最后一课！我们证明环中的另一条经典性质：**负元乘法的符号规则**。具体目标：`(-a) * b = -(a * b)` 直观上，「负 a 乘以 b」应该等于「a 乘以 b 的相反数」。这和中学代数中 `(-a) * b = -(a * b)` 的规则一致。这个证明用到的技巧和前几课密切相关——分配律 + 加法群性质。你已经有了一切所需工具！

本关学到的新东西

概念 (Concepts)

add_comm加法交换律。a + b = b + a

add_neg加法逆元。a + (-a) = 0

环中的符号规则(-a)*b = -(a*b)。从分配律和加法群公理可证

证明目标

当前目标

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

⊢(-a) * b = -(a * b)

分步提示

1.要证 `(-a) * b = -(a * b)`。在环中，`x = -y` 的一个充分条件是 `x + y = 0`。所以策略是证 `(-a) * b + (a * b) = 0`。
2.`calc (-a) * b + (a * b) = ((-a) + a) * b := by rw [right_distrib]`，用右分配律把两项合并。
3.`((-a) + a) * b` 中的 `(-a) + a` 是什么？根据加法交换律和 `add_neg`，`(-a) + a = a + (-a) = 0`。
4.`rw [add_comm (-a) a, add_neg a]` 得到 `0 * b`。而 `0 * b = 0`——这已经在第 17 课说明过。这里我们直接用 `rw` 一个环公理或 `sorry`。
5.实际上在基本环公理中我们不一定有 `0 * b = 0`，但可以通过同样的技巧证明：`0 * b = (0+0)*b = 0*b+0*b`，消去得 `0*b=0`。这里我们用 `calc` 完整写出。

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

Lean 代码编辑器