Elementary number theory

Files in the elementary number theory folder

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-rationals 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-ring-of-integers 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.decidable-dependent-function-types public
open import elementary-number-theory.decidable-total-order-natural-numbers public
open import elementary-number-theory.decidable-types public
open import elementary-number-theory.difference-integers 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.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.fibonacci-sequence 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.groups-of-modular-arithmetic public
open import elementary-number-theory.half-integers 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.kolakoski-sequence 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.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-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.multiset-coefficients public
open import elementary-number-theory.natural-numbers public
open import elementary-number-theory.nonzero-natural-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.pisano-periods 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.sieve-of-eratosthenes public
open import elementary-number-theory.square-free-natural-numbers public
open import elementary-number-theory.stirling-numbers-of-the-second-kind public
open import elementary-number-theory.strict-inequality-natural-numbers 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.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-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