Schanuel's Conjecture

Reference: Wikipedia

theorem Schanuel.adjoin_trdeg_le_of_finite {A : Type u_1} {ι : Type u_2} [Field A] {S : Set A} (hS : S.Finite) : Algebra.trdeg A ↥(IntermediateField.adjoin A S) ≤ ↑S.ncard

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

theorem Schanuel.schanuel_conjecture (n : ℕ) (z : Fin n → ℂ) (h : LinearIndependent ℚ z) : have hinj := ⋯; ↑n ≤ Algebra.trdeg ℚ ↥(IntermediateField.adjoin ℚ (Set.range z ∪ Set.range (Complex.exp ∘ z)))

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}$.