Gelfond-Schneider theorem

Stream: maths

[Michail Karatarakis]

I have a formalisation of the Gelfond–Schneider Theorem which solves Hilbert’s Seventh Problem: namely, that for an algebraic number $\alpha \neq 0, 1$ and irrational algebraic $\beta,$ the number $\alpha ^ \beta$ is transcendental.

It needs some refactoring; I’m happy to polish it and submit a PR.
https://github.com/mkaratarakis/mathlib4/tree/final/Mathlib/NumberTheory/Transcendental/GelfondSchneider

[Johan Commelin]

Congrats! And wowzerz, the main file is > 6K LOC!

[Kevin Buzzard]

Congratulations Michail! As Johan points out, that is not a PR, that is more like 50 PRs, if we're talking about mathlib (and I don't see why it shouldn't be there). You might want to start by making PRs adding basic API which was missing from defintions already present in mathlib.