Documentation

Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart

Analytic part of the Lindemann-Weierstrass theorem #

See equation (68), page 285 of [Jacobson, Basic Algebra I, 4.12][jacobson1974].

Given a polynomial f with integer coefficients, we can find a constant c : ℝ and for each prime p > |f₀|, nₚ : ℤ and gₚ : ℤ[X] such that

  • p does not divide nₚ
  • deg(gₚ) < p * deg(f)
  • all complex roots r of f satisfy |nₚ * e ^ r - p * gₚ(r)| ≤ c ^ p / (p - 1)!

In the proof of Lindemann-Weierstrass, we will take f to be a polynomial whose complex roots are the algebraic numbers whose exponentials we want to prove to be linearly independent.

Note: Jacobson writes Nₚ for our nₚ and M for our c (modulo a constant factor).