The triangular numbers
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-02-16.
Last modified on 2023-05-13.
module elementary-number-theory.triangular-numbers where
Imports
open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers
Definition
triangular-number-ℕ : ℕ → ℕ triangular-number-ℕ 0 = 0 triangular-number-ℕ (succ-ℕ n) = (triangular-number-ℕ n) +ℕ (succ-ℕ n)
Recent changes
- 2023-05-13. Fredrik Bakke. Refactor to use infix binary operators for arithmetic (#620).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).
- 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).
- 2023-03-05. Jonathan Prieto-Cubides. Add “suggest an edit” button and minor fix (#484).