# Sequences of the online encyclopedia of integer sequences

Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.

Created on 2023-03-21.

module online-encyclopedia-of-integer-sequences.oeis where

Imports
open import elementary-number-theory.ackermann-function
open import elementary-number-theory.cofibonacci
open import elementary-number-theory.collatz-bijection
open import elementary-number-theory.eulers-totient-function
open import elementary-number-theory.exponentiation-natural-numbers
open import elementary-number-theory.factorials
open import elementary-number-theory.fibonacci-sequence
open import elementary-number-theory.infinitude-of-primes
open import elementary-number-theory.kolakoski-sequence
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.pisano-periods

open import finite-group-theory.finite-groups

open import foundation.function-types


## Sequences

### A000001 The number of groups of order n

A000001 : ℕ → ℕ
A000001 = number-of-groups-of-order


### A000002 The Kolakoski sequence

A000002 : ℕ → ℕ
A000002 = kolakoski


### A000010 Euler's totient function

A000010 : ℕ → ℕ
A000010 = eulers-totient-function-relatively-prime


### A000040 The prime numbers

A000040 : ℕ → ℕ
A000040 = prime-ℕ


### A000045 The Fibonacci sequence

A000045 : ℕ → ℕ
A000045 = Fibonacci-ℕ


### A000079 Powers of 2

A000079 : ℕ → ℕ
A000079 = exp-ℕ 2


### A000142 Factorials

A000142 : ℕ → ℕ
A000142 = factorial-ℕ


### A000244 Powers of 3

A000244 : ℕ → ℕ
A000244 = exp-ℕ 3


### A000720 The prime counting function

A000720 : ℕ → ℕ
A000720 = prime-counting-ℕ


### A001175 Pisano periods

A001175 : ℕ → ℕ
A001175 = pisano-period


### A001177 The cofibonacci sequence

A001177 : ℕ → ℕ
A001177 = cofibonacci


### A001477 The natural numbers

A001477 : ℕ → ℕ
A001477 = id


### A006369 Collatz' bijection

A006369 : ℕ → ℕ
A006369 = map-collatz-bijection


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

A046859 : ℕ → ℕ
A046859 n = ackermann n n