编辑“︁Lean代数库”︁

= Lean代数库 =

'''Lean代数库'''是[[Lean定理证明器]]数学库（mathlib）的核心组成部分之一，专注于抽象代数结构的定义、定理和计算。它为群论、环论、域论、模论等代数分支提供形式化支持，并广泛应用于数学证明和程序验证。

== 核心概念 ==

=== 代数结构的定义 ===
Lean代数库通过'''类型类'''（Type Classes）实现代数结构的层次化组织。例如，一个'''群'''（Group）被定义为具有结合律、单位元和逆元的'''幺半群'''（Monoid）：

<syntaxhighlight lang="lean">
class Group (G : Type u) extends Monoid G where
  inv : G → G
  mul_left_inv : ∀ a : G, a * inv a = 1
</syntaxhighlight>

=== 常用代数结构 ===
以下是Lean中部分关键结构的类型类层次：
<mermaid>
classDiagram
  Semigroup <|-- Monoid
  Monoid <|-- Group
  Monoid <|-- CommMonoid
  Group <|-- CommGroup
  AddGroup <|-- AddCommGroup
  Ring <|-- CommRing
  Module <|-- VectorSpace
</mermaid>

== 代码示例 ==

=== 群的基本操作 ===
<syntaxhighlight lang="lean">
-- 定义整数加法群实例
instance : AddCommGroup ℤ where
  add := Int.add
  add_assoc := Int.add_assoc
  zero := 0
  zero_add := Int.zero_add
  add_zero := Int.add_zero
  neg := Int.neg
  add_left_neg := Int.add_left_neg
  add_comm := Int.add_comm

-- 使用群公理证明简单引理
example (a b : ℤ) : a + b - b = a := by
  rw [add_sub_cancel]
</syntaxhighlight>
'''输出'''：目标状态直接简化为<code>a = a</code>，通过<code>rw</code>（重写）策略应用代数库中的预置定理。

=== 多项式环运算 ===
<syntaxhighlight lang="lean">
import Mathlib.Algebra.Polynomial

-- 在ℤ[X]中计算(x+1)^2
example : Polynomial ℤ :=
  (X + 1) ^ 2  -- 展开结果为 X^2 + 2*X + 1
</syntaxhighlight>

== 实际应用案例 ==

=== 密码学验证 ===
在椭圆曲线密码学中，Lean代数库可用于证明群运算性质：
<syntaxhighlight lang="lean">
-- 定义椭圆曲线点加法结合律
theorem ec_add_assoc (P Q R : ECPoint) :
  (P + Q) + R = P + (Q + R) := by
  apply ec_group.add_assoc  -- 调用代数库中的群公理
</syntaxhighlight>

=== 线性代数计算 ===
利用模论进行矩阵运算验证：
<syntaxhighlight lang="lean">
import Mathlib.LinearAlgebra.Matrix

-- 证明矩阵乘法的分配律
example (A B C : Matrix n n ℝ) :
  A * (B + C) = A * B + A * C :=
  Matrix.mul_add A B C  -- 直接调用代数库定理
</syntaxhighlight>

== 数学公式支持 ==
代数库中的定理常涉及复杂公式，例如'''第一同构定理'''：
<math>
G/\ker \phi \cong \operatorname{im} \phi
</math>
在Lean中对应的形式化语句：
<syntaxhighlight lang="lean">
theorem quotient_ker_equiv_range (φ : G →* H) :
  G ⧸ ker φ ≃* range φ := ...
</syntaxhighlight>

== 学习建议 ==

* 从基础结构（如Semigroup）逐步学习类型类继承体系
* 使用<code>#check</code>命令查看代数对象的类型签名
* 结合Mathlib文档中的`Algebra.Group.Basic`等文件进行实践

代数库的设计体现了Lean的'''分层抽象'''理念，既支持高阶的范畴论概念，也提供具体的数值计算工具。通过逐步探索不同抽象层次，用户可以深入理解形式化代数的强大能力。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean与数学库]]