Lindemann–Weierstrass theorem

TheoremLindemann–Weierstrass theorem (universe-polymorphic form)#✓fully proved

Let \(\iota\) be a finite index set, let \(\alpha_i\) (\(i \in \iota\)) be pairwise distinct complex numbers that are algebraic over \(\mathbb{Q}\), and let \(\beta_i\) (\(i \in \iota\)) be complex numbers that are algebraic over \(\mathbb{Q}\) and not all zero. Then \(\sum_{i \in \iota} \beta_i e^{\alpha_i} \neq 0\).

public theorem lindemann_weierstrass' :
    ∀ {ι : Type*} [Fintype ι] (α : ι → ℂ),
      Function.Injective α → (∀ i, IsAlgebraic ℚ (α i)) →
        ∀ (β : ι → ℂ), (∀ i, IsAlgebraic ℚ (β i)) → (∃ i, β i ≠ 0) →
          ∑ i, β i * Complex.exp (α i) ≠ 0

Used by 1

Used byLindemann–Weierstrass theorem

TheoremLindemann–Weierstrass theorem#✓fully proved

Let \(\iota\) be a finite index set, let \(\alpha_i\) (\(i \in \iota\)) be pairwise distinct complex numbers that are algebraic over \(\mathbb{Q}\), and let \(\beta_i\) (\(i \in \iota\)) be complex numbers that are algebraic over \(\mathbb{Q}\) and not all zero. Then \(\sum_{i \in \iota} \beta_i e^{\alpha_i} \neq 0\).

public theorem lindemann_weierstrass :
    ∀ {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → ℂ),
      Function.Injective α → (∀ i, IsAlgebraic ℚ (α i)) →
        ∀ (β : ι → ℂ), (∀ i, IsAlgebraic ℚ (β i)) → (∃ i, β i ≠ 0) →
          ∑ i, β i * Complex.exp (α i) ≠ 0

Sources

• F. von Lindemann 1882 and K. Weierstrass, Zu Lindemann's Abhandlung Über die Ludolph'sche Zahl, 1885; textbook in Baker, Transcendental Number Theory

Uses 1

Proof usesLindemann–Weierstrass theorem (universe-polymorphic form)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.