Telephone numbers

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Eléonore Mangel.

Created on 2022-03-24.
Last modified on 2023-05-13.

module elementary-number-theory.telephone-numbers where
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers


The telephone numbers are a sequence of natural numbers that count the way n telephone lines can be connected to each other, where each line can be connected to at most one other line. They also occur in several other combinatorics problems.


telephone-number :   
telephone-number zero-ℕ = succ-ℕ zero-ℕ
telephone-number (succ-ℕ zero-ℕ) = succ-ℕ zero-ℕ
telephone-number (succ-ℕ (succ-ℕ n)) =
  (telephone-number (succ-ℕ n)) +ℕ ((succ-ℕ n) *ℕ (telephone-number n))

Recent changes