Map · 12
field theory
MSC 12 · Field theory and polynomials
7,767 declarations (6,595 theorems, 1,172 definitions) across 221 files. 9 of the 19 famous theorems listed for this area are in Mathlib (47%). 18 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.
Subareas6
- 12E General field theory 3,563
- 12F Field extensions 2,948
- 12J Topological fields 858
- 12D Real and complex fields 347
- 12H Differential and difference algebra 28
- 12K Generalizations of fields 23
Famous theorems9 of 19
From the 1000+ theorems project, which classifies each theorem by MSC area.
Not yet in Mathlib · 10
In Mathlib · 9
- Abel–Ruffini theoremAbelRuffini.exists_not_solvable_by_rad
- Chevalley–Warning theoremchar_dvd_card_solutions_of_sum_lt
- Integral root theoremisInteger_of_is_root_of_monic
- Mason–Stothers theoremPolynomial.abc
- Primitive element theoremField.exists_primitive_element
- Rational root theoremnum_dvd_of_is_root
- Schwartz–Zippel theoremMvPolynomial.schwartz_zippel_sup_sum
- Solutions of a general cubic equationTheorems100.cubic_eq_zero_iff
- Solutions of a general quartic equationTheorems100.quartic_eq_zero_iff
From the 100 theorems list3
Open conjectures stated in Lean18
Statements without proofs, collected by the Formal Conjectures project.
- Erdos1150.erdos_1150Erdős Problems
- Erdos477.erdos_477Erdős Problems
- Erdos477.erdos_477.variants.X_pow_threeErdős Problems
- Erdos477.erdos_477.variants.monomialErdős Problems
- Erdos522.erdos_522Erdős Problems
- Erdos522.erdos_522.variants.zero_oneErdős Problems
- EulerBrick.cuboidThreeWikipedia
- EulerBrick.cuboidTwoWikipedia
Structures defined here24
Typeclasses defined in this area's files, most assumed first.
- Field 12,076
- NontriviallyNormedField 10,032
- NormedField 1,842
- DivisionRing 1,377
- Semifield 536
- NormedDivisionRing 400
- Algebra.IsAlgebraic 314
- DivisionSemiring 276
- Algebra.IsSeparable 221
- PerfectRing 211
- IsAlgClosed 166
- IsGalois 140
- Normal 106
- IsPurelyInseparable 75
- IsSepClosed 55
- IsPRadical 49
- PerfectField 48
- Polynomial.IsSplittingField 40
- IsAlgClosure 31
- DenselyNormedField 21
- SubfieldClass 19
- IsPurelyInseparable.HasExponent 15
- IsAbelianGalois 13
- IsRealClosed 13
Files221
Largest first. The code after each file is its assigned subarea.
- Mathlib.Algebra.Polynomial.Basic
Theory of univariate polynomials
12E · 274
- Mathlib.Data.Complex.Basic
The complex numbers
12D · 240
- Mathlib.FieldTheory.IntermediateField.Basic
Intermediate fields
12F · 197
- Mathlib.Algebra.Polynomial.Eval.Defs
Evaluating a polynomial
12E · 160
- Mathlib.Algebra.Polynomial.Roots
Theory of univariate polynomials
12E · 159
- Mathlib.FieldTheory.RatFunc.Basic
The field structure of rational functions
12E · 156
- Mathlib.Algebra.Polynomial.AlgebraMap
Theory of univariate polynomials
12E · 138
- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Adjoining Elements to Fields
12F · 138
- Mathlib.Algebra.Polynomial.Degree.Operations
Lemmas for calculating the degree of univariate polynomials
12E · 132
- Mathlib.Data.Real.Basic
Real numbers from Cauchy sequences
12J · 124
- Mathlib.Algebra.Polynomial.Degree.Defs
Degree of univariate polynomials
12E · 121
- Mathlib.Algebra.CubicDiscriminant
Cubics and discriminants
12E · 114