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