Skip to content

Commit

Permalink
Move OEIS to literature (#1208)
Browse files Browse the repository at this point in the history
This PR moves the OEIS module to the literature
  • Loading branch information
EgbertRijke authored Oct 24, 2024
1 parent e249655 commit ffdf33c
Show file tree
Hide file tree
Showing 7 changed files with 68 additions and 71 deletions.
10 changes: 6 additions & 4 deletions references.bib
Original file line number Diff line number Diff line change
Expand Up @@ -488,10 +488,12 @@ @misc{Mye21
primaryclass = {math.CT}
}

@online{OEIS,
title = {The {{On-Line Encyclopedia}} of {{Integer Sequences}} ({{OEIS}})},
organization = {{{OEIS}} Foundation Inc.},
url = {https://oeis.org/}
@online{oeis,
title = {The {{On-Line Encyclopedia}} of {{Integer Sequences}}},
author = {OEIS Foundation Inc.},
date = {1996},
url = {https://oeis.org},
howpublished = {website},
}

@book{Rie17,
Expand Down
25 changes: 19 additions & 6 deletions src/elementary-number-theory/ackermann-function.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,14 +15,27 @@ open import elementary-number-theory.natural-numbers
## Idea

The
{{#concept "Ackermann function" WD="Ackermann function" WDID=Q341835 Agda=ackermann}}
is a fast growing binary operation on the natural numbers.
{{#concept "Ackermann-Péter function" WD="Ackermann function" WDID=Q341835 Agda=ackermann-péter-ℕ}}
is a fast growing binary operation on the
[natural numbers](elementary-number-theory.natural-numbers.md).

## Definition

### The Ackermann-Péter function

```agda
ackermann-péter-ℕ :
ackermann-péter-ℕ zero-ℕ n =
succ-ℕ n
ackermann-péter-ℕ (succ-ℕ m) zero-ℕ =
ackermann-péter-ℕ m 1
ackermann-péter-ℕ (succ-ℕ m) (succ-ℕ n) =
ackermann-péter-ℕ m (ackermann-péter-ℕ (succ-ℕ m) n)
```

### The simplified Ackermann function

```agda
ackermann :
ackermann zero-ℕ n = succ-ℕ n
ackermann (succ-ℕ m) zero-ℕ = ackermann m 1
ackermann (succ-ℕ m) (succ-ℕ n) = ackermann m (ackermann (succ-ℕ m) n)
simplified-ackermann-ℕ :
simplified-ackermann-ℕ n = ackermann-péter-ℕ n n
```
4 changes: 2 additions & 2 deletions src/elementary-number-theory/euclid-mullin-sequence.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,8 @@ by
euclid-mullin-ℕ 0 := 2,
```

and `euclid-mullin-ℕ (n + 1)` is the least [prime
factor](elementary-number-theory.prime numbers.md) of the product of all
and `euclid-mullin-ℕ (n + 1)` is the least
[prime factor](elementary-number-theory.prime-numbers.md) of the product of all
previous entries in the Euclid–Mullin sequence plus one.

## Definitions
Expand Down
2 changes: 1 addition & 1 deletion src/elementary-number-theory/fermat-numbers.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ are numbers of the form $F_n := 2^{2^n}+1$. The first five Fermat numbers are
```

The sequence of Fermat numbers is listed as A000215 in the
[Online Encyclopedia of Integer Sequences](online-encyclopedia-of-integer-sequences.oeis.md).
[Online Encyclopedia of Integer Sequences](literature.oeis.md).

Alternatively, the Fermat numbers can be defined with
[strong induction](elementary-number-theory.strong-induction-natural-numbers.md)
Expand Down
3 changes: 2 additions & 1 deletion src/literature.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,11 @@ module literature where

open import literature.100-theorems public
open import literature.idempotents-in-intensional-type-theory public
open import literature.oeis public
open import literature.sequential-colimits-in-homotopy-type-theory public
```

## References

{{#bibliography}} {{#reference SvDR20}} {{#reference Shu17}}
{{#reference 100theorems}}
{{#reference 100theorems}} {{#reference oeis}}
Original file line number Diff line number Diff line change
@@ -1,33 +1,19 @@
# Sequences of the online encyclopedia of integer sequences

This file records formalized sequences of the
[Online Encyclopedia of Integer Sequences](https://oeis.org) {{#cite oeis}}.

```agda
module online-encyclopedia-of-integer-sequences.oeis where
module literature.oeis where
```

<details><summary>Imports</summary>

```agda
open import elementary-number-theory.ackermann-function
open import elementary-number-theory.catalan-numbers
open import elementary-number-theory.cofibonacci
open import elementary-number-theory.collatz-bijection
open import elementary-number-theory.euclid-mullin-sequence
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.fermat-numbers
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.multiset-coefficients
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

open import univalent-combinatorics.main-classes-of-latin-squares
```

</details>
Expand All @@ -37,15 +23,15 @@ open import univalent-combinatorics.main-classes-of-latin-squares
### [A000001](https://oeis.org/A000001) The number of groups of order `n`

```agda
A000001 :
A000001 = number-of-groups-of-order
open import finite-group-theory.finite-groups using
( number-of-groups-of-order)
```

### [A000002](https://oeis.org/A000002) The Kolakoski sequence

```agda
A000002 :
A000002 = kolakoski
open import elementary-number-theory.kolakoski-sequence using
( kolakoski)
```

### [A000004](https://oeis.org/A000004) The zero sequence
Expand All @@ -66,8 +52,8 @@ A000007 (succ-ℕ _) = 0
### [A000010](https://oeis.org/A000010) Euler's totient function

```agda
A000010 :
A000010 = eulers-totient-function-relatively-prime
open import elementary-number-theory.eulers-totient-function using
( eulers-totient-function-relatively-prime)
```

### [A000012](https://oeis.org/A000012) All 1's sequence
Expand All @@ -87,15 +73,15 @@ A000027 = succ-ℕ
### [A000040](https://oeis.org/A000040) The prime numbers

```agda
A000040 :
A000040 = prime-ℕ
open import elementary-number-theory.infinitude-of-primes using
( prime-ℕ)
```

### [A000045](https://oeis.org/A000045) The Fibonacci sequence

```agda
A000045 :
A000045 = Fibonacci-ℕ
open import elementary-number-theory.fibonacci-sequence using
( Fibonacci-ℕ)
```

### [A000079](https://oeis.org/A000079) Powers of `2`
Expand All @@ -108,22 +94,22 @@ A000079 = exp-ℕ 2
### [A000108](https://oeis.org/A000108) The Catalan numbers

```agda
A000108 :
A000108 = catalan-numbers
open import elementary-number-theory.catalan-numbers using
( catalan-numbers)
```

### [A000142](https://oeis.org/A000142) Factorials

```agda
A000142 :
A000142 = factorial-ℕ
open import elementary-number-theory.factorials using
( factorial-ℕ)
```

### [A000215](https://oeis.org/A000215) The Fermat numbers

```agda
A000215 :
A000215 = fermat-number-ℕ
open import elementary-number-theory.fermat-numbers using
( fermat-number-ℕ)
```

### [A000244](https://oeis.org/A000244) Powers of `3`
Expand All @@ -136,29 +122,29 @@ A000244 = exp-ℕ 3
### [A000720](https://oeis.org/A000720) The prime counting function

```agda
A000720 :
A000720 = prime-counting-ℕ
open import elementary-number-theory.infinitude-of-primes using
( prime-counting-ℕ)
```

### [A000945](https://oeis.org/A000945) The Euclid–Mullin sequence

```agda
A000945 :
A000945 = euclid-mullin-ℕ
open import elementary-number-theory.euclid-mullin-sequence using
( euclid-mullin-ℕ)
```

### [A001175](https://oeis.org/A001175) Pisano periods

```agda
A001175 :
A001175 = pisano-period
open import elementary-number-theory.pisano-periods using
( pisano-period)
```

### [A001177](https://oeis.org/A001177) The cofibonacci sequence

```agda
A001177 :
A001177 = cofibonacci
open import elementary-number-theory.cofibonacci using
( cofibonacci)
```

### [A001477](https://oeis.org/A001477) The natural numbers
Expand All @@ -171,20 +157,24 @@ A001477 = id
### [A003090](https://oeis.org/A003090) The number of main classes of Latin squares of order `n`

```agda
A003090 :
A003090 = number-of-main-classes-of-Latin-squares-of-order
open import univalent-combinatorics.main-classes-of-latin-squares using
( number-of-main-classes-of-Latin-squares-of-order)
```

### [A006369](https://oeis.org/A006369) Collatz' bijection

```agda
A006369 :
A006369 = map-collatz-bijection
open import elementary-number-theory.collatz-bijection using
( map-collatz-bijection)
```

### [A046859](https://oeis.org/A046859) The main diagonal of the Ackermann–Péter function

```agda
A046859 :
A046859 n = ackermann n n
open import elementary-number-theory.ackermann-function using
( simplified-ackermann-ℕ)
```

## References

{{#bibliography}}
9 changes: 0 additions & 9 deletions src/online-encyclopedia-of-integer-sequences.lagda.md

This file was deleted.

0 comments on commit ffdf33c

Please sign in to comment.