Gelfond–Schneider theorem

TheoremGelfond–Schneider theorem for every value of a complex power#✓fully proved

Let \(a, b \in \mathbb{C}\) be algebraic over \(\mathbb{Q}\) with \(a \neq 1\) and \(b \notin \mathbb{Q}\), and let \(z \in \mathbb{C}\) satisfy \(e^z = a\). Then \(e^{bz}\) is transcendental over \(\mathbb{Q}\).

The hypothesis \(e^z = a\) already implies \(a \neq 0\). Taking \(z = \log a + 2 \pi i n\), where \(\log a\) is the principal logarithm and \(n\) is an integer, recovers every branch of \(a^b\).

theorem gelfondSchneider_complex_exp :
    ∀ {a b z : ℂ}, IsAlgebraic ℚ a → IsAlgebraic ℚ b → a ≠ 1 →
      b ∉ Set.range (algebraMap ℚ ℂ) → Complex.exp z = a →
        Transcendental ℚ (Complex.exp (b * z))

Sources

• A. O. Gelfond, Sur le septième problème de Hilbert (1934), and T. Schneider, Transzendenzuntersuchungen periodischer Funktionen I. Transzendenz von Potenzen, J. Reine Angew. Math. 172 (1935), 65–69, DOI 10.1515/crll.1935.172.65. Explicit arbitrary- and principal-branch applications occur in arXiv:2311.11127v1, arXiv:2607.23662v1, and arXiv:2608.17545v1. The Lean formalization in arXiv:2603.24823v1 states only the principal Complex.cpow value; this declaration records the arbitrary-logarithm form.

Used by 1

Used byGelfond–Schneider theorem for real powers

TheoremGelfond–Schneider theorem for real powers#✓fully proved

Let \(\alpha\) and \(\beta\) be real numbers that are algebraic over \(\mathbb{Q}\), with \(\alpha > 0\), \(\alpha \neq 1\) and \(\beta\) irrational. Then the real power \(\alpha^\beta\) is transcendental over \(\mathbb{Q}\).

theorem gelfondSchneider_real_rpow :
    ∀ (α β : ℝ), 0 < α → α ≠ 1 → IsAlgebraic ℚ α → IsAlgebraic ℚ β →
      Irrational β → Transcendental ℚ (Real.rpow α β)

Sources

• A. O. Gelfond, Sur le septième problème de Hilbert, Dokl. Akad. Nauk SSSR 2 (1934) 1–6 and T. Schneider 1935 independent; textbook in Baker, Transcendental Number Theory

Uses 1

Proof usesGelfond–Schneider theorem for every value of a complex power

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.