Sequences of the online encyclopedia of integer sequences

Content created by Egbert Rijke.

Created on 2024-10-24.
Last modified on 2024-10-25.

This file records formalized sequences of the Online Encyclopedia of Integer Sequences [OEIS].

module literature.oeis where
Imports 
open import elementary-number-theory.exponentiation-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.function-types

Sequences

A000001 The number of groups of order n

open import finite-group-theory.finite-groups using
  ( number-of-groups-of-order)

A000002 The Kolakoski sequence

open import elementary-number-theory.kolakoski-sequence using
  ( kolakoski)

A000004 The zero sequence

A000004 : ℕ → ℕ
A000004 _ = zero-ℕ

A000007 The characteristic function for 0

A000007 : ℕ → ℕ
A000007 zero-ℕ = 1
A000007 (succ-ℕ _) = 0

A000010 Euler’s totient function

open import elementary-number-theory.eulers-totient-function using
  ( eulers-totient-function-relatively-prime)

A000012 All 1’s sequence

A000012 : ℕ → ℕ
A000012 _ = 1

A000027 The positive integers

A000027 : ℕ → ℕ
A000027 = succ-ℕ

A000040 The prime numbers

open import elementary-number-theory.infinitude-of-primes using
  ( prime-ℕ)

A000045 The Fibonacci sequence

open import elementary-number-theory.fibonacci-sequence using
  ( Fibonacci-ℕ)

A000058 Sylvester’s sequence

open import elementary-number-theory.sylvesters-sequence using
  ( sylvesters-sequence-ℕ)

A000079 Powers of 2

A000079 : ℕ → ℕ
A000079 = exp-ℕ 2

A000108 The Catalan numbers

open import elementary-number-theory.catalan-numbers using
  ( catalan-numbers)

A000142 Factorials

open import elementary-number-theory.factorials using
  ( factorial-ℕ)

A000215 The Fermat numbers

open import elementary-number-theory.fermat-numbers using
  ( fermat-number-ℕ)

A000244 Powers of 3

A000244 : ℕ → ℕ
A000244 = exp-ℕ 3

A000720 The prime counting function

open import elementary-number-theory.infinitude-of-primes using
  ( prime-counting-ℕ)

A000945 The Euclid–Mullin sequence

open import elementary-number-theory.euclid-mullin-sequence using
  ( euclid-mullin-ℕ)

A001175 Pisano periods

open import elementary-number-theory.pisano-periods using
  ( pisano-period)

A001177 The cofibonacci sequence

open import elementary-number-theory.cofibonacci using
  ( cofibonacci)

A001477 The natural numbers

A001477 : ℕ → ℕ
A001477 = id

A003090 The number of main classes of Latin squares of order n

open import univalent-combinatorics.main-classes-of-latin-squares using
  ( number-of-main-classes-of-Latin-squares-of-order)

A006369 Collatz’ bijection

open import elementary-number-theory.collatz-bijection using
  ( map-collatz-bijection)

A046859 The main diagonal of the Ackermann–Péter function

open import elementary-number-theory.ackermann-function using
  ( simplified-ackermann-ℕ)

References

[OEIS]
OEIS Foundation Inc. The On-Line Encyclopedia of Integer Sequences. website. URL: https://oeis.org.

Recent changes