Triangular sum

Definition

SumOfCubesPractice_triangleSum

by hacv16 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-sumsnumber-theorypractice

For every natural number $n$ , define

\operatorname{triangleSum}(n)=\sum_{k=1}^{n}k.

The sum includes both endpoints and is zero when $n=0$ . This function provides the shared sum of positive integers used in the three theorem statements.

Definition code

import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Order.Interval.Finset.Nat

open scoped BigOperators

namespace SumOfCubesPractice

def triangleSum (n : ℕ) : ℕ :=
  ∑ k ∈ Finset.Icc 1 n, k

end SumOfCubesPractice

Source

Requester-supplied mathematical statement for Sum of Cubes Identity (Practice); no external bibliographic source supplied. Definitions: triangleSum.

Read-back

What the Lean code literally says, in plain math · Codex, based on GPT-6 (exact model identifier unavailable)

The function $T:\mathbb{N}\to\mathbb{N}$ , named SumOfCubesPractice.triangleSum, assigns to each natural number $n$ the sum $T(n)=\sum_{k=1}^{n}k$ over all natural numbers $k$ satisfying $1\le k\le n$ , with the sum taken in the natural numbers. The input $n=0$ is included; then the index set is empty and $T(0)=0$ .

View graph