编辑“︁Lean数论基础”︁（章节）

== 基本概念 ==  

=== 整除性与模运算 ===  
在数论中，'''整除性'''（Divisibility）是一个核心概念。若整数<math>a</math>能被整数<math>b</math>整除（记作<math>b \mid a</math>），则存在整数<math>k</math>使得<math>a = b \cdot k</math>。在Lean中，可以通过以下方式定义：

<syntaxhighlight lang="lean">
-- 定义整除性
def divides (a b : ℤ) : Prop := ∃ k, b = a * k

-- 示例：证明 2 整除 4
example : divides 2 4 :=
begin
  use 2,  -- 存在 k = 2 使得 4 = 2 * 2
  norm_num,
end
</syntaxhighlight>

'''模运算'''（Modular Arithmetic）是另一个重要概念，表示整数除法后的余数。在Lean中，可以使用`%`运算符或定义等价关系：

<syntaxhighlight lang="lean">
-- 计算 7 mod 3
#eval 7 % 3  -- 输出: 1

-- 定义模等价
def mod_equiv (a b n : ℤ) : Prop := n ∣ (a - b)
</syntaxhighlight>

=== 素数 ===  
'''素数'''（Prime Numbers）是大于1且只有1和自身两个正因数的自然数。Lean的标准库`mathlib`提供了素数的定义：

<syntaxhighlight lang="lean">
import data.nat.prime

-- 检查 5 是否为素数
#eval nat.prime 5  -- 输出: true

-- 证明 7 是素数
example : nat.prime 7 :=
begin
  norm_num,  -- 通过计算验证
end
</syntaxhighlight>