Elementary number theory

Content created by Egbert Rijke, Fredrik Bakke, malarbol, Fernando Chu, Alec Barreto, Jonathan Prieto-Cubides, Elif Uskuplu, Julian KG, Maša Žaucer, Victor Blanchi, Vojtěch Štěpančík and Gregor Perčič.

Created on 2022-01-28.
Last modified on 2024-11-04.

Modules in the elementary number theory namespace

module elementary-number-theory where

open import elementary-number-theory.absolute-value-integers public
open import elementary-number-theory.ackermann-function public
open import elementary-number-theory.addition-integer-fractions public
open import elementary-number-theory.addition-integers public
open import elementary-number-theory.addition-natural-numbers public
open import elementary-number-theory.addition-positive-and-negative-integers public
open import elementary-number-theory.addition-rational-numbers public
open import elementary-number-theory.additive-group-of-rational-numbers public
open import elementary-number-theory.arithmetic-functions public
open import elementary-number-theory.based-induction-natural-numbers public
open import elementary-number-theory.based-strong-induction-natural-numbers public
open import elementary-number-theory.bezouts-lemma-integers public
open import elementary-number-theory.bezouts-lemma-natural-numbers public
open import elementary-number-theory.binomial-coefficients public
open import elementary-number-theory.binomial-theorem-integers public
open import elementary-number-theory.binomial-theorem-natural-numbers public
open import elementary-number-theory.bounded-sums-arithmetic-functions public
open import elementary-number-theory.catalan-numbers public
open import elementary-number-theory.cofibonacci public
open import elementary-number-theory.collatz-bijection public
open import elementary-number-theory.collatz-conjecture public
open import elementary-number-theory.commutative-semiring-of-natural-numbers public
open import elementary-number-theory.congruence-integers public
open import elementary-number-theory.congruence-natural-numbers public
open import elementary-number-theory.cross-multiplication-difference-integer-fractions public
open import elementary-number-theory.cubes-natural-numbers public
open import elementary-number-theory.decidable-dependent-function-types public
open import elementary-number-theory.decidable-total-order-integers public
open import elementary-number-theory.decidable-total-order-natural-numbers public
open import elementary-number-theory.decidable-total-order-rational-numbers public
open import elementary-number-theory.decidable-total-order-standard-finite-types public
open import elementary-number-theory.decidable-types public
open import elementary-number-theory.difference-integers public
open import elementary-number-theory.difference-rational-numbers public
open import elementary-number-theory.dirichlet-convolution public
open import elementary-number-theory.distance-integers public
open import elementary-number-theory.distance-natural-numbers public
open import elementary-number-theory.divisibility-integers public
open import elementary-number-theory.divisibility-modular-arithmetic public
open import elementary-number-theory.divisibility-natural-numbers public
open import elementary-number-theory.divisibility-standard-finite-types public
open import elementary-number-theory.equality-integers public
open import elementary-number-theory.equality-natural-numbers public
open import elementary-number-theory.euclid-mullin-sequence public
open import elementary-number-theory.euclidean-division-natural-numbers public
open import elementary-number-theory.eulers-totient-function public
open import elementary-number-theory.exponentiation-natural-numbers public
open import elementary-number-theory.factorials public
open import elementary-number-theory.falling-factorials public
open import elementary-number-theory.fermat-numbers public
open import elementary-number-theory.fibonacci-sequence public
open import elementary-number-theory.field-of-rational-numbers public
open import elementary-number-theory.finitary-natural-numbers public
open import elementary-number-theory.finitely-cyclic-maps public
open import elementary-number-theory.fundamental-theorem-of-arithmetic public
open import elementary-number-theory.goldbach-conjecture public
open import elementary-number-theory.greatest-common-divisor-integers public
open import elementary-number-theory.greatest-common-divisor-natural-numbers public
open import elementary-number-theory.group-of-integers public
open import elementary-number-theory.half-integers public
open import elementary-number-theory.hardy-ramanujan-number public
open import elementary-number-theory.inequality-integer-fractions public
open import elementary-number-theory.inequality-integers public
open import elementary-number-theory.inequality-natural-numbers public
open import elementary-number-theory.inequality-rational-numbers public
open import elementary-number-theory.inequality-standard-finite-types public
open import elementary-number-theory.infinitude-of-primes public
open import elementary-number-theory.initial-segments-natural-numbers public
open import elementary-number-theory.integer-fractions public
open import elementary-number-theory.integer-partitions public
open import elementary-number-theory.integers public
open import elementary-number-theory.jacobi-symbol public
open import elementary-number-theory.kolakoski-sequence public
open import elementary-number-theory.legendre-symbol public
open import elementary-number-theory.lower-bounds-natural-numbers public
open import elementary-number-theory.maximum-natural-numbers public
open import elementary-number-theory.maximum-standard-finite-types public
open import elementary-number-theory.mediant-integer-fractions public
open import elementary-number-theory.mersenne-primes public
open import elementary-number-theory.minimum-natural-numbers public
open import elementary-number-theory.minimum-standard-finite-types public
open import elementary-number-theory.modular-arithmetic public
open import elementary-number-theory.modular-arithmetic-standard-finite-types public
open import elementary-number-theory.monoid-of-natural-numbers-with-addition public
open import elementary-number-theory.monoid-of-natural-numbers-with-maximum public
open import elementary-number-theory.multiplication-integer-fractions public
open import elementary-number-theory.multiplication-integers public
open import elementary-number-theory.multiplication-lists-of-natural-numbers public
open import elementary-number-theory.multiplication-natural-numbers public
open import elementary-number-theory.multiplication-positive-and-negative-integers public
open import elementary-number-theory.multiplication-rational-numbers public
open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers public
open import elementary-number-theory.multiplicative-group-of-rational-numbers public
open import elementary-number-theory.multiplicative-inverses-positive-integer-fractions public
open import elementary-number-theory.multiplicative-monoid-of-natural-numbers public
open import elementary-number-theory.multiplicative-monoid-of-rational-numbers public
open import elementary-number-theory.multiplicative-units-integers public
open import elementary-number-theory.multiplicative-units-standard-cyclic-rings public
open import elementary-number-theory.multiset-coefficients public
open import elementary-number-theory.natural-numbers public
open import elementary-number-theory.negative-integers public
open import elementary-number-theory.nonnegative-integers public
open import elementary-number-theory.nonpositive-integers public
open import elementary-number-theory.nonzero-integers public
open import elementary-number-theory.nonzero-natural-numbers public
open import elementary-number-theory.nonzero-rational-numbers public
open import elementary-number-theory.ordinal-induction-natural-numbers public
open import elementary-number-theory.parity-natural-numbers public
open import elementary-number-theory.peano-arithmetic public
open import elementary-number-theory.pisano-periods public
open import elementary-number-theory.poset-of-natural-numbers-ordered-by-divisibility public
open import elementary-number-theory.positive-and-negative-integers public
open import elementary-number-theory.positive-integer-fractions public
open import elementary-number-theory.positive-integers public
open import elementary-number-theory.positive-rational-numbers public
open import elementary-number-theory.powers-integers public
open import elementary-number-theory.powers-of-two public
open import elementary-number-theory.prime-numbers public
open import elementary-number-theory.products-of-natural-numbers public
open import elementary-number-theory.proper-divisors-natural-numbers public
open import elementary-number-theory.pythagorean-triples public
open import elementary-number-theory.rational-numbers public
open import elementary-number-theory.reduced-integer-fractions public
open import elementary-number-theory.relatively-prime-integers public
open import elementary-number-theory.relatively-prime-natural-numbers public
open import elementary-number-theory.repeating-element-standard-finite-type public
open import elementary-number-theory.retracts-of-natural-numbers public
open import elementary-number-theory.ring-of-integers public
open import elementary-number-theory.ring-of-rational-numbers public
open import elementary-number-theory.sieve-of-eratosthenes public
open import elementary-number-theory.square-free-natural-numbers public
open import elementary-number-theory.squares-integers public
open import elementary-number-theory.squares-modular-arithmetic public
open import elementary-number-theory.squares-natural-numbers public
open import elementary-number-theory.standard-cyclic-groups public
open import elementary-number-theory.standard-cyclic-rings public
open import elementary-number-theory.stirling-numbers-of-the-second-kind public
open import elementary-number-theory.strict-inequality-integer-fractions public
open import elementary-number-theory.strict-inequality-integers public
open import elementary-number-theory.strict-inequality-natural-numbers public
open import elementary-number-theory.strict-inequality-rational-numbers public
open import elementary-number-theory.strict-inequality-standard-finite-types public
open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers public
open import elementary-number-theory.strong-induction-natural-numbers public
open import elementary-number-theory.sums-of-natural-numbers public
open import elementary-number-theory.sylvesters-sequence public
open import elementary-number-theory.taxicab-numbers public
open import elementary-number-theory.telephone-numbers public
open import elementary-number-theory.triangular-numbers public
open import elementary-number-theory.twin-prime-conjecture public
open import elementary-number-theory.type-arithmetic-natural-numbers public
open import elementary-number-theory.unit-elements-standard-finite-types public
open import elementary-number-theory.unit-similarity-standard-finite-types public
open import elementary-number-theory.universal-property-integers public
open import elementary-number-theory.universal-property-natural-numbers public
open import elementary-number-theory.upper-bounds-natural-numbers public
open import elementary-number-theory.well-ordering-principle-natural-numbers public
open import elementary-number-theory.well-ordering-principle-standard-finite-types public

Recent changes