如何在Lean中使用求和符号Σ？含导入要求与定理示例写法

依赖导入 #

要使用大西格玛求和符号，首先需要导入对应的mathlib模块，同时打开相关命名空间即可直接使用Σ语法：

-- 导入求和语法核心依赖
import Mathlib.Algebra.BigOperators.Basic
-- 如需使用自然数区间范围，额外导入该模块
import Mathlib.Data.Nat.Interval

-- 打开命名空间，省略前缀直接使用Σ语法
open Finset
open BigOperators

在Lean编辑器中，输入\sum即可快速输入Σ符号。

求和表达式编写规则 #

• 通用语法为：Σ 变量 ∈ 有限集合, 求和项
  其中有限集合指定求和的遍历范围，求和项是基于遍历变量计算的表达式
• 常用范围写法：
  • 遍历前n个自然数（0到n-1）：使用range n作为范围
  • 遍历闭区间[a, b]的所有自然数（包含a和b）：使用Icc a b作为范围
• 求和符号优先级符合数学书写习惯，无需额外加括号也能正常识别复杂求和项

示例定理补全 #

你要求的「前n个自然数（从1到n）之和等于n * (n + 1) / 2」的定理，补全后代码如下：

theorem exmpl (n : ℕ) : (Σ k ∈ Icc 1 n, k) = n * (n + 1) / 2 := by
  -- 此处可补充证明逻辑
  sorry

如果你的求和范围是从0到n的自然数，只需要将范围替换为range (n + 1)即可。

内容的提问来源于stack exchange，提问作者502E532E