Analytic part of the Lindemann-Weierstrass theorem

The proof is partially based on Jacobson, Basic Algebra I, 4.12.

theorem LindemannWeierstrass.exp_polynomial_approx (f : Polynomial ℤ) (hf : Polynomial.eval 0 f ≠ 0) : ∃ (c : ℝ), ∀ p > (Polynomial.eval 0 f).natAbs, Nat.Prime p → ∃ (nₚ : ℤ), ¬↑p ∣ nₚ ∧ ∃ (gₚ : Polynomial ℤ), gₚ.natDegree ≤ p * f.natDegree - 1 ∧ ∀ {r : ℂ}, r ∈ f.aroots ℂ → ‖nₚ • Complex.exp r - p • (Polynomial.aeval r) gₚ‖ ≤ c ^ p / ↑(p - 1).factorial

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) - 1 (note: deg(gₚ) < p * deg(f) is not true if f is a nonzero constant polynomial)
• 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 (equation (68) / lemma 3, page 285) writes Nₚ for our nₚ and M for our c (modulo a constant factor).