Field Theory

InstanceField \(\Q\) of rational numbers#

Mathlib states this as Rat.instField.

Rat.instField : Field ℚ
Sources
MathlibRat.instField
Uses 2 · Used by 14
Statement usesField · Rational number
Used byFormula for Pythagorean Triples · Insolvability of General Higher Degree Equations (Abel-Ruffini Theorem) · The Non-Denumerability of the Continuum · Solutions to Pell’s Equation (Freek Wiedijk's 100 theorems) · Sum of the Reciprocals of the Triangular Numbers · Sum of kth powers · Stirling’s Formula · Ahlswede-Zhang identity · Translation numbers define a group action up to semiconjugacy · Mahler's theorem · Ostrowski's theorem · Poisson limit theorem · Matrix exponential · Hilbert projection theorem

InstanceField \(\R\) of real numbers#

Mathlib states this as Real.instField.

Real.instField : Field ℝ
Sources
MathlibReal.instField
Uses 1 · Used by 36
Statement usesReal number
Used byLiouville’s Theorem and the Construction of Transcendental Numbers · The Irrationality of the Square Root of 2 · Divergence of the Harmonic Series · The Ballot Problem · L’Hopital’s Rule · Sum of a Geometric Series · The Mean Value Theorem (Freek Wiedijk's 100 theorems) · Theorem of Ceva · Rolle's theorem · Finite-dimensional normed spaces over complete normed fields are complete · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Triangle counting lemma · Uniqueness of integral curves · Chebyshev inequality · Urysohn's lemma · Uniformly continuous function · Gershgorin circle theorem · Darboux's theorem (analysis) · Cauchy–Hadamard theorem · M. Riesz extension theorem · Apollonius's theorem · Krein–Milman theorem · Beatty's theorem · Ostrowski's theorem · Sylvester's law of inertia (existence) · Field \(\C\) of complex numbers · Complex exponential · Continuity (Complex-valued series) · Convergence of \(p\)-series for \(p>1\) · Differentiability of the limit of a sequence of functions · Weierstrass polynomial approximation theorem · Taylor's theorem with Lagrange form for remainder · Completeness of R · Completeness of \(l^2\) · Limits of sequences · Topology of a metric space

InstanceField \(\C\) of complex numbers#

Mathlib states this as Complex.instField.

Complex.instField : Field ℂ
Sources
MathlibComplex.instField
Uses 2 · Used by 18
Statement usesComplex number · Field \(\R\) of real numbers
Used byDe Moivre’s Formula · Insolvability of General Higher Degree Equations (Abel-Ruffini Theorem) · Fourier Series · Fundamental theorem of algebra · Riemann-Lebesgue lemma (Analysis) · Abel's theorem · Fernique's theorem · Gauss–Lucas theorem · Fourier theorem · Niven's theorem · Lévy continuity theorem · Cyclotomic polynomials in \(\Q[X]\) · Cos (power series expansion of elementary functions) · Log · Sin (power series expansion of elementary functions) · Cauchy formulas · Holomorphic stability under uniform convergence · Weierstrass trigonometric approximation theorem

DefinitionAlgebraic elements#

An element of an R-algebra is algebraic over R if it is a root of a nonzero polynomial with coefficients in R.

IsAlgebraic.{u, v} (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (x : A) : Prop
Sources
MathlibIsAlgebraic
Uses 3 · Used by 3
Statement usesAssociative algebra over a commutative ring · Linear map · Polynomial in one indeterminate
Used byInsolvability of General Higher Degree Equations (Abel-Ruffini Theorem) · Algebraic extension · Transcendental elements

DefinitionTranscendental elements#

An element of an R-algebra is transcendental over R if it is not algebraic over R.

Transcendental.{u, v} (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (x : A) : Prop
Sources
MathlibTranscendental
Uses 1 · Used by 2
Statement usesAlgebraic elements
Used byLiouville’s Theorem and the Construction of Transcendental Numbers · Liouville's theorem on existence of transcendental numbers

DefinitionFinite fields#

This file contains basic results about finite fields. Throughout most of this file, K denotes a finite field and q is notation for the cardinality of K.

Mathlib covers this with the module Mathlib.FieldTheory.Finite.Basic rather than a single declaration.

Its 28 documented declarations include FiniteField.card_image_polynomial_eval, FiniteField.exists_root_sum_quadratic, FiniteField.sum_subgroup_units_eq_zero, FiniteField.sum_subgroup_units, FiniteField.card, FiniteField.sum_pow_units, FiniteField.sum_pow_lt_card_sub_one, FiniteField.frobeniusAlgHom, FiniteField.frobeniusAlgEquiv, FiniteField.frobeniusAlgEquivOfAlgebraic, Nat.sq_add_sq_zmodEq, Nat.sq_add_sq_modEq, and 16 more.

Sources
MathlibFiniteField.card_image_polynomial_eval · FiniteField.exists_root_sum_quadratic · FiniteField.sum_subgroup_units_eq_zero · FiniteField.sum_subgroup_units · FiniteField.card · FiniteField.sum_pow_units · FiniteField.sum_pow_lt_card_sub_one · FiniteField.frobeniusAlgHom · FiniteField.frobeniusAlgEquiv · FiniteField.frobeniusAlgEquivOfAlgebraic · Nat.sq_add_sq_zmodEq · Nat.sq_add_sq_modEq
Used by 1
Used byChevalley-Warning theorem (Number theory)

StructureRational fraction fields with one indeterminate over a field#

RatFunc K is K(X), the field of rational functions over K.

The inclusion of polynomials into RatFunc is algebraMap K[X] K⟮X⟯, the maps between K⟮X⟯ and another field of fractions of K[X], especially FractionRing K[X], are given by IsLocalization.algEquiv.

RatFunc.{u} (K : Type u) [CommRing K] : Type u
Sources
MathlibRatFunc
Uses 2 · Used by 2
Statement usesLocalization · Polynomial in one indeterminate
Used byOstrowski's theorem · Rational functions

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.