FTA - "algebraic" proof

Stream: Is there code for X?

[Artie Khovanov]

Does anyone know of any formalisation of the "algebraic" (Galois theoretic) proof of FTA? This is the one that starts with the analytic claims that, in the reals, any positive number has a square root, and any odd-degree polynomial has a root, and proceeds purely algebraically, using Galois theory and Sylow's theorems, to show that the only nontrivial algebraic extension of the reals is quadratic and moreover given by adjoining a square root of -1.

For context, I'm trying to formalise some real algebra, specifically the theory of real closed fields, so it would be good to just generalise this proof. I don't think this proof is in Mathlib, but maybe it's in someone else's open source repo?

[Johan Commelin]

I'm not aware of this proof being done in Lean.