Sequences of the online encyclopedia of integer sequences

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

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.functions

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

A000040 The prime numbers

A000040 : ℕ → ℕ
A000040 = prime-ℕ

A000045 The Fibonacci sequence

A000045 : ℕ → ℕ
A000045 = Fibonacci-ℕ

A000079 Powers of 2

A000079 : ℕ → ℕ
A000079 = exp-ℕ 

A000142 Factorials

A000142 : ℕ → ℕ
A000142 = factorial-ℕ

A000244 Powers of 3

A000244 : ℕ → ℕ
A000244 = exp-ℕ 

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