Polygonal numbers

DefinitionPolygonal numbers#✓fully proved

For natural numbers \(s\) and \(n\), the \(n\)-th \(s\)-gonal number is \(p_s(n) = (s - 2)\binom{n}{2} + n\), where \(s - 2\) is truncated subtraction of natural numbers (so it is \(0\) when \(s < 2\)).

The polygonal interpretation assumes \(s \ge 3\); this definition extends the formula to every natural number \(s\).

def polygonalNumber (s n : ℕ) : ℕ := (s - 2) * Nat.choose n 2 + n

Used by 19

Used byLarge integers as a practical number plus two polygonal numbers · Sums of two polygonal numbers modulo an odd prime · Parity of sums of two polygonal numbers · Every positive integer is a practical number plus a triangular number · Sums of two polygonal numbers modulo prime powers · Quadratic upper bound for polygonal numbers · Exceptions to sums of a practical number and polygonal numbers · Odd squares and triangular numbers · Gauss's Eureka theorem · Fermat polygonal number theorem · Polygonal numbers at four · Polygonal numbers at three · Polygonal numbers at two · Closed form of the pentagonal numbers · Square numbers as polygonal numbers · Polygonal numbers at one · Closed form of the hexagonal numbers · Closed form of the triangular numbers · Polygonal numbers at zero

TheoremPolygonal numbers at zero#✓fully proved

For every natural number \(s\), \(p_s(0) = 0\), where \(p_s(n)\) is the \(n\)-th \(s\)-gonal number.

The source considers only \(s \ge 3\); the value holds for the extension of the formula to every natural number \(s\).

@[simp] theorem polygonalNumber_zero (s : ℕ) : polygonalNumber s 0 = 0

Uses 1

Statement usesPolygonal numbers

TheoremPolygonal numbers at one#✓fully proved

For every natural number \(s\), \(p_s(1) = 1\), where \(p_s(n)\) is the \(n\)-th \(s\)-gonal number.

The source considers only \(s \ge 3\); the value holds for the extension of the formula to every natural number \(s\).

@[simp] theorem polygonalNumber_one (s : ℕ) : polygonalNumber s 1 = 1

Uses 1 · Used by 1

Statement usesPolygonal numbers

Used byFermat polygonal number theorem

TheoremPolygonal numbers at two#✓fully proved

For every natural number \(s \ge 3\), \(p_s(2) = s\), where \(p_s(n)\) is the \(n\)-th \(s\)-gonal number.

theorem polygonalNumber_at_two (s : ℕ) (hs : 3 ≤ s) : polygonalNumber s 2 = s

Uses 1

Statement usesPolygonal numbers

TheoremPolygonal numbers at three#✓fully proved

For every natural number \(s \ge 3\), \(p_s(3) = 3s - 3\), where \(p_s(n)\) is the \(n\)-th \(s\)-gonal number.

theorem polygonalNumber_at_three (s : ℕ) (hs : 3 ≤ s) :
    polygonalNumber s 3 = 3 * s - 3

Uses 1

Statement usesPolygonal numbers

TheoremPolygonal numbers at four#✓fully proved

For every natural number \(s \ge 3\), \(p_s(4) = 6s - 8\), where \(p_s(n)\) is the \(n\)-th \(s\)-gonal number.

theorem polygonalNumber_at_four (s : ℕ) (hs : 3 ≤ s) :
    polygonalNumber s 4 = 6 * s - 8

Uses 1

Statement usesPolygonal numbers

TheoremClosed form of the triangular numbers#✓fully proved

For every natural number \(n\), the \(n\)-th triangular number is \(p_3(n) = \frac{n(n + 1)}{2}\), where \(p_s(n)\) is the \(n\)-th \(s\)-gonal number.

The quotient is exact, since \(n(n + 1)\) is even.

theorem polygonalNumber_three (n : ℕ) :
    polygonalNumber 3 n = n * (n + 1) / 2

Uses 1 · Used by 1

Statement usesPolygonal numbers

Used byGauss's Eureka theorem

TheoremSquare numbers as polygonal numbers#✓fully proved

For every natural number \(n\), the \(n\)-th square number is \(p_4(n) = n^2\), where \(p_s(n)\) is the \(n\)-th \(s\)-gonal number.

theorem polygonalNumber_four (n : ℕ) : polygonalNumber 4 n = n ^ 2

Uses 1 · Used by 1

Statement usesPolygonal numbers

Used byFermat polygonal number theorem

TheoremClosed form of the pentagonal numbers#✓fully proved

For every natural number \(n\), the \(n\)-th pentagonal number is \(p_5(n) = \frac{3n^2 - n}{2}\), where \(p_s(n)\) is the \(n\)-th \(s\)-gonal number.

The quotient is exact, since \(3n^2 - n = n(3n - 1)\) is even.

theorem polygonalNumber_five (n : ℕ) :
    polygonalNumber 5 n = (3 * n ^ 2 - n) / 2

Uses 1

Statement usesPolygonal numbers

TheoremClosed form of the hexagonal numbers#✓fully proved

For every natural number \(n\), the \(n\)-th hexagonal number is \(p_6(n) = 2n^2 - n\), where \(p_s(n)\) is the \(n\)-th \(s\)-gonal number.

theorem polygonalNumber_six (n : ℕ) :
    polygonalNumber 6 n = 2 * n ^ 2 - n

Uses 1

Statement usesPolygonal numbers

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.