Schanuel's Conjecture

Reference: Wikipedia

@[reducible, inline]

noncomputable abbrev Schanuel.transcendenceDegree (R : Type u_1) {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (h : Function.Injective ⇑(algebraMap R A)) : ℕ

The transcendence degree of an $A$-algebra is the common cardinality of transcendence bases.

Equations

• Schanuel.transcendenceDegree R h = Set.univ.ncard

theorem Schanuel.isTranscendenceBasis_ncard_eq_transcendenceDegree (R : Type u_1) {A : Type u_2} {ι : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (h : Function.Injective ⇑(algebraMap R A)) (𝒷 : ι → A) (hS : IsTranscendenceBasis R 𝒷) : Set.univ.ncard = transcendenceDegree R h

The transcendence degree is independent of the choice of a transcendence basis.

theorem Schanuel.adjoin_transcendenceDegree_le_of_finite {A : Type u_1} {ι : Type u_2} [Field A] {S : Set A} (hS : S.Finite) : transcendenceDegree A ⋯ ≤ S.ncard

The transcendence degree of $A$ adjoined $\{x_1, ..., x_n\}$ is $\leq n$.

theorem Schanuel.schanuel_conjecture (n : ℕ) (z : Fin n → ℂ) (h : LinearIndependent ℚ z) : let hinj := ⋯; n ≤ transcendenceDegree ℚ hinj

Given any set of $n$ complex numbers $\{z_1, ..., z_n\}$ that are linearly independent over $\mathbb{Q}$, the field extension $\mathbb{Q}(z_1, ..., z_n, e^{z_1}, ..., e^{z_n})$ has transcendence degree at least $n$ over $\mathbb{Q}$.