syntax - 如何在精益中使用求和符号？

Question

在精益中，存在一种求和符号(Σ，大西格玛)的符号，用于写出包含许多项的求和。可悲的是，mathlib documentation 都不是也不是 reference manual似乎提供了很多关于如何使用它的信息。

为了使用它需要什么导入，你如何用它写总和？

例如，您将如何使用求和符号写出第一个 n 自然数加起来等于 n * (n + 1)/2 的定理？

theorem exmpl (n : ℕ) : --(sum from k=1 to k=n over term n) = n * (n + 1) / 2

Answer 1

Yury 的回答很好，但请注意，他们使用病态的(对数学家而言)函数 nat.div 来对自然数进行除法；例如，此函数具有 9/2 = 4 的属性，因为它输出自然。计算机科学家可能已经习惯了这一点，但我倾向于鼓励数学家不惜一切代价避免使用这个函数，因为他们已经习惯了像 a/b * b = a 这样的事情是真的，而这不是nat.div 为真。如果您首先强制进入有理数，那么您将使用 rat.div ，它以非病态(对数学家)的方式表现。要证明上面 Yury 的结果，您需要绕道去证明，例如，n*(n+1) 总是偶数。将此方法与有理数进行比较，后者很容易消失:

import tactic

open_locale big_operators

open finset

-- sum from i = 0 to n-1 of i^3 is (n(n-1)/2)^2
example (n : ℕ) : (∑ i in range n, i^3 : ℚ) = (n*(n-1)/2)^2 :=
begin
  induction n with d hd,
  { simp, ring },
  { rw [sum_range_succ, hd],
    simp, ring }
end

换句话说，证明是“明显的归纳法”，精益证明的短小表明没有其他事情发生。