Sequences of the online encyclopedia of integer sequences

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