Map · 11
number theory
MSC 11 · Number theory
14,549 declarations (12,011 theorems, 2,538 definitions) across 494 files. 27 of the 127 famous theorems listed for this area are in Mathlib (21%), 31 in some Lean library. 983 open conjectures here are stated in Lean.
Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.
Subareas17
- 11A Elementary number theory 5,042
- 11R Algebraic number theory: global fields 2,971
- 11F Discontinuous groups and automorphic forms 1,211
- 11S Algebraic number theory: local fields 884
- 11B Sequences and sets 850
- 11M Zeta and \(L\)-functions: analytic theory 757
- 11T Finite fields and commutative rings (number-theoretic aspects) 716
- 11E Forms and linear algebraic groups 499
- 11G Arithmetic algebraic geometry (Diophantine geometry) 482
- 11D Diophantine equations 351
- 11N Multiplicative number theory 240
- 11J Diophantine approximation, transcendental number theory 160
- 11L Exponential sums and character sums 147
- 11H Geometry of numbers 131
- 11P Additive number theory; partitions 90
- 11C Polynomials and matrices 14
- 11Y Computational number theory 4
Famous theorems27 of 127
From the 1000+ theorems project, which classifies each theorem by MSC area.
Not yet in Mathlib · 100
In Mathlib · 27
- Beatty's theoremIrrational.beattySeq_symmDiff_beattySeq_pos
- Bertrand's postulateNat.bertrand
- Chinese remainder theoremIdeal.quotientInfRingEquivPiQuotient
- Corners theoremcorners_theorem_nat
- Dirichlet's approximation theoremAddCircle.exists_norm_nsmul_le
- Dirichlet's theorem on arithmetic progressionsNat.infinite_setOf_prime_and_eq_mod
- Dirichlet's unit theoremNumberField.Units.basisModTorsion
- Erdős–Ginzburg–Ziv theoremZMod.erdos_ginzburg_ziv
- Euclid's theoremNat.exists_infinite_primes
- Euclid–Euler theoremTheorems100.Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect
- Euler's partition theoremNat.Partition.card_odds_eq_card_distincts
- Euler's theoremNat.ModEq.pow_totient
From the 100 theorems list20
- 1. The Irrationality of the Square Root of 2
- 7. Law of Quadratic Reciprocity
- 10. Euler’s Generalization of Fermat’s Little Theorem
- 11. The Infinitude of Primes
- 14. Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + ….
- 18. Liouville’s Theorem and the Construction of Transcendental Numbers
- 19. Four Squares Theorem
- 20. All Primes (1 mod 4) Equal the Sum of Two Squares
- 23. Formula for Pythagorean Triples
- 39. Solutions to Pell’s Equation
- 40. Minkowski’s Fundamental Theorem
- 45. The Partition Theorem
- 48. Dirichlet’s Theorem
- 51. Wilson’s Lemma
- 60. Bezout’s Theorem
- 77. Sum of kth powers
- 80. The Fundamental Theorem of Arithmetic
- 81. Divergence of the Prime Reciprocal Series
- 85. Divisibility by 3 Rule
- 98. Bertrand’s Postulate
Open conjectures stated in Lean983
Statements without proofs, collected by the Formal Conjectures project.
- ABC.abcWikipedia
- ABC.abc.variants.lt_constant_mulWikipedia
- ABC.abc.variants.qualityWikipedia
- AgohGiuga.agoh_giugaWikipedia
- AgohGiuga.agoh_giuga.variants.giugaWikipedia
- AgrawalConjecture.agrawal_conjectureWikipedia
Structures defined here24
Typeclasses defined in this area's files, most assumed first.
- NumberField 805
- LinearOrderedCommGroupWithZero 741
- IsCyclotomicExtension 234
- LinearOrderedCommMonoidWithZero 207
- Height.AdmissibleAbsValues 122
- ModularFormClass 87
- Subgroup.HasDetPlusMinusOne 79
- HasEnoughRootsOfUnity 63
- Subgroup.IsArithmetic 53
- NumberField.IsCMField 50
- Subgroup.HasDetOne 38
- IsZLattice 35
- NNRatCast 26
- SlashInvariantFormClass 26
- CuspFormClass 25
- NumberField.IsTotallyReal 21
- Northcott 18
- WeierstrassCurve.IsIntegral 18
- NumberField.IsTotallyComplex 16
- IsDecompositionField 15
- IsNonarchimedeanLocalField 15
- Zsqrtd.Nonsquare 15
- IsHeckeTriple 14
- WittVector.Isocrystal 12
Files494
Largest first. The code after each file is its assigned subarea.
- Mathlib.LinearAlgebra.QuadraticForm.Basic
Quadratic maps
11E · 227
- Mathlib.Data.ZMod.Basic
Integers mod `n`
11T · 210
- Mathlib.NumberTheory.ModularForms.Basic
Modular forms
11F · 170
11R · 168
- Mathlib.Data.Num.Basic
Binary representation of integers using inductive types
11A · 164
- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Canonical embedding of a number field
11R · 153
- Mathlib.NumberTheory.Padics.PadicNumbers
p-adic numbers
11S · 152
- Mathlib.Algebra.Order.GroupWithZero.Canonical
Linearly ordered commutative groups and monoids with a zero element adjoined
11R · 150
- Mathlib.Data.Num.Lemmas
Properties of the binary representation of integers
11A · 142
- Mathlib.NumberTheory.Divisors
Divisor Finsets
11A · 133
- Mathlib.Data.Num.Bitwise
Bitwise operations using binary representation of integers
11A · 121
- Mathlib.Data.Nat.ModEq
Congruences modulo a natural number
11A · 120