12 Field theory and polynomials

TheoremChevalley–Warning theorem (1000+ theorems)#

The Chevalley–Warning theorem, finitary version. Let (f i) be a finite family of multivariate polynomials in finitely many variables (X s, s : σ) over a finite field of characteristic p. Assume that the sum of the total degrees of the f i is less than the cardinality of σ. Then the number of common solutions of the f i is divisible by p.

char_dvd_card_solutions_of_sum_lt.{u_1, u_2, u_3} {K : Type u_1} {σ : Type u_2} {ι : Type u_3}
  [Fintype K] [Field K] [Fintype σ] [DecidableEq σ] [DecidableEq K] (p : ℕ) [CharP K p]
  {s : Finset ι} {f : ι → MvPolynomial σ K} (h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ) :
  p ∣ Fintype.card { x // ∀ i ∈ s, (MvPolynomial.eval x) (f i) = 0 }
Sources
Mathlibchar_dvd_card_solutions_of_sum_lt
Uses 5 · Used by 1
Statement usesCharacteristic p · Field · Polynomial in several indeterminates · Rational number · Ring morphism
Used byErdős–Ginzburg–Ziv theorem

TheoremIntegral root theorem#

Integral root theorem: if r : f.codomain is a root of a monic polynomial over the ufd A, then r is an integer

isInteger_of_is_root_of_monic.{u_1, u_2} {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A]
  [UniqueFactorizationMonoid A] [Field K] [Algebra A K] [IsFractionRing A K] {p : Polynomial A}
  (hp : p.Monic) {r : K} (hr : (Polynomial.aeval r) p = 0) : IsLocalization.IsInteger A r
Sources
MathlibisInteger_of_is_root_of_monic
Uses 7 · Used by 1
Statement usesAssociative algebra over a commutative ring · Field of fractions of an integral domain · Linear map · Polynomial in one indeterminate · Rational number · Unique factorisation domain
Proof usesRational root theorem
Used byNiven's theorem

TheoremMason–Stothers theorem#

Polynomial ABC theorem.

Polynomial.abc.{u_1} {k : Type u_1} [Field k] [DecidableEq k] {a b c : Polynomial k} (ha : a ≠ 0)
  (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) (hsum : a + b + c = 0) :
  a.natDegree + 1 ≤ (UniqueFactorizationMonoid.radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (UniqueFactorizationMonoid.radical (a * b * c)).natDegree ∧
        c.natDegree + 1 ≤ (UniqueFactorizationMonoid.radical (a * b * c)).natDegree ∨
    Polynomial.derivative a = 0 ∧ Polynomial.derivative b = 0 ∧ Polynomial.derivative c = 0
Sources
MathlibPolynomial.abc
Uses 7
Statement uses\(K[X]\) is Euclidean · Coprime element · Greatest common divisor · Least common multiple · Polynomial derivative · Rational number · The Fundamental Theorem of Arithmetic

TheoremPrimitive element theorem#

Primitive element theorem: a finite separable field extension E of F has a primitive element, i.e. there is an α ∈ E such that F⟮α⟯ = (⊤ : Subalgebra F E).

Field.exists_primitive_element.{u_1, u_2} (F : Type u_1) (E : Type u_2) [Field F] [Field E]
  [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] : ∃ α, F⟮α⟯ = ⊤
Sources
MathlibField.exists_primitive_element
Uses 9
Statement usesFinite-dimensionality · Minimal polynomial · Separable polynomial · Subfield
Proof uses\(K[X]\) is Euclidean · Cyclic group · Greatest Common Divisor Algorithm · Local ring · Splitting field

TheoremRational root theorem#

Mathlib records this with 2 declarations.

num_dvd_of_is_root: Rational root theorem part 1: if r : f.codomain is a root of a polynomial over the ufd A, then the numerator of r divides the constant coefficient

num_dvd_of_is_root.{u_1, u_2} {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A]
  [UniqueFactorizationMonoid A] [Field K] [Algebra A K] [IsFractionRing A K] {p : Polynomial A}
  {r : K} (hr : (Polynomial.aeval r) p = 0) : IsFractionRing.num A r ∣ p.coeff 0

den_dvd_of_is_root: Rational root theorem part 2: if r : f.codomain is a root of a polynomial over the ufd A, then the denominator of r divides the leading coefficient

den_dvd_of_is_root.{u_1, u_2} {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A]
  [UniqueFactorizationMonoid A] [Field K] [Algebra A K] [IsFractionRing A K] {p : Polynomial A}
  {r : K} (hr : (Polynomial.aeval r) p = 0) : ↑(IsFractionRing.den A r) ∣ p.leadingCoeff
Sources
Mathlibnum_dvd_of_is_root · den_dvd_of_is_root
Uses 7 · Used by 1
Statement usesAssociative algebra over a commutative ring · Field of fractions of an integral domain · Linear map · Polynomial in one indeterminate · Rational number · Unique factorisation domain
Proof usesPolynomial functions
Used byIntegral root theorem

TheoremSchwartz–Zippel theorem#

The Schwartz-Zippel lemma

For a nonzero multivariable polynomial p over an integral domain, the probability that p evaluates to zero at points drawn at random from a product of finite subsets S i of the integral domain is bounded by the supremum of ∑ i, degᵢ s / #(S i) ranging over monomials s of p.

MvPolynomial.schwartz_zippel_sup_sum.{u_1} {R : Type u_1} [CommRing R] [IsDomain R] [DecidableEq R]
  {n : ℕ} {p : MvPolynomial (Fin n) R} (hp : p ≠ 0) (S : Fin n → Finset R) :
  ↑{x ∈ Fintype.piFinset fun i => S i | (MvPolynomial.eval x) p = 0}.card / ∏ i, ↑(S i).card ≤
    p.support.sup fun s => ∑ i, ↑(s i) / ↑(S i).card
Sources
MathlibMvPolynomial.schwartz_zippel_sup_sum
Uses 7
Statement usesPolynomial in several indeterminates · Rational number · Ring morphism
Proof usesAssociative algebra over a commutative ring · Characteristic p · Ordered ring · Roots of a polynomial

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.