跳到主要内容

Lean 代数库

Lean是一种交互式定理证明器，同时也是一种功能强大的编程语言。它的代数库（Mathlib）为数学和计算机科学中的代数结构提供了丰富的支持。本文将带你了解Lean代数库的基础知识，并通过代码示例和实际案例帮助你掌握其核心概念。

什么是Lean代数库？​

Lean的代数库（Mathlib）是一个庞大的数学库，涵盖了从基础代数到高级数学的广泛内容。它提供了定义和操作代数结构（如群、环、域等）的工具，并支持对这些结构进行形式化证明。

对于初学者来说，Lean代数库是一个强大的工具，可以帮助你理解抽象的代数概念，并通过代码实践加深对这些概念的理解。

基本概念​

群（Group）​

群是代数中最基本的结构之一。一个群由一个集合和一个二元运算组成，满足以下性质：

  1. 结合律：对于所有 a, b, c，有 (a * b) * c = a * (b * c)。
  2. 单位元：存在一个元素 e，使得对于所有 a，有 e * a = a * e = a。
  3. 逆元：对于每个元素 a，存在一个元素 a⁻¹，使得 a * a⁻¹ = a⁻¹ * a = e。

在Lean中，群的定义如下：

class group (G : Type*) :=
(mul : G → G → G)
(one : G)
(inv : G → G)
(mul_assoc : ∀ a b c : G, mul (mul a b) c = mul a (mul b c))
(one_mul : ∀ a : G, mul one a = a)
(mul_one : ∀ a : G, mul a one = a)
(inv_mul : ∀ a : G, mul (inv a) a = one)

环（Ring）​

环是另一个重要的代数结构，它由一个集合和两个二元运算（加法和乘法）组成，满足以下性质：

  1. 加法群：集合关于加法形成一个交换群。
  2. 乘法半群：集合关于乘法形成一个半群（即乘法满足结合律）。
  3. 分配律：乘法对加法满足分配律。

在Lean中，环的定义如下：

class ring (R : Type*) :=
(add : R → R → R)
(zero : R)
(neg : R → R)
(mul : R → R → R)
(add_assoc : ∀ a b c : R, add (add a b) c = add a (add b c))
(zero_add : ∀ a : R, add zero a = a)
(add_zero : ∀ a : R, add a zero = a)
(add_comm : ∀ a b : R, add a b = add b a)
(mul_assoc : ∀ a b c : R, mul (mul a b) c = mul a (mul b c))
(left_distrib : ∀ a b c : R, mul a (add b c) = add (mul a b) (mul a c))
(right_distrib : ∀ a b c : R, mul (add a b) c = add (mul a c) (mul b c))

实际案例​

案例1：整数环​

整数集合 ℤ 关于加法和乘法形成一个环。我们可以使用Lean来验证这一点。

import algebra.ring

instance : ring ℤ :=
{ add := int.add,
  zero := 0,
  neg := int.neg,
  mul := int.mul,
  add_assoc := int.add_assoc,
  zero_add := int.zero_add,
  add_zero := int.add_zero,
  add_comm := int.add_comm,
  mul_assoc := int.mul_assoc,
  left_distrib := int.distrib_left,
  right_distrib := int.distrib_right }

案例2：矩阵环​

矩阵集合 Mₙ(R) 关于矩阵加法和矩阵乘法也形成一个环。我们可以定义一个2x2矩阵的环结构。

import data.matrix.basic

variables (R : Type*) [ring R]

instance : ring (matrix (fin 2) (fin 2) R) :=
{ add := matrix.add,
  zero := matrix.zero,
  neg := matrix.neg,
  mul := matrix.mul,
  add_assoc := matrix.add_assoc,
  zero_add := matrix.zero_add,
  add_zero := matrix.add_zero,
  add_comm := matrix.add_comm,
  mul_assoc := matrix.mul_assoc,
  left_distrib := matrix.mul_add,
  right_distrib := matrix.add_mul }

总结​

Lean代数库为数学中的代数结构提供了强大的支持。通过本文的介绍，你应该对群、环等基本概念有了初步的了解，并能够使用Lean来定义和操作这些结构。

附加资源​

练习​

  1. 尝试在Lean中定义一个交换群（Abelian Group）。
  2. 验证实数集合 ℝ 关于加法和乘法是否形成一个域（Field）。

通过不断练习，你将能够更深入地理解Lean代数库，并在数学和计算机科学中应用这些知识。