Theorems · Theorem · number theory

Liouville.exists_pos_real_of_irrational_root

∀ {α : ℝ},
  Irrational α →
    ∀ {f : Polynomial ℤ},
      f ≠ 0 →
        Polynomial.eval α (Polynomial.map (algebraMap ℤ ℝ) f) = 0 →
          ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)

Defined in

Mathlib.NumberTheory.Transcendental.Liouville.Basic

Cited by

1 results in Mathlib

Foundations

Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound