Generator of intermediate Field of degree 2

Stream: Is there code for X?

[Ludwig Monnerjahn]

I have two intermediate fields $L$, $K$ of $E$ and $F$ with $K \le L$ and $[L:K]=2$ is there a lemma which gives me that $L=K(x)$ for some $x\in L$ with $x\cdot x \in K$. In my case $E$ and $F$ are $\mathbb{Q}$ and $\mathbb{C}$ so the extension is separable.

[Floris van Doorn]

You have a higher chance that someone helps you if you provide a Lean statement as part of your question.

[Scott Carnahan]

You also need 2 to be invertible (which holds in your case).

[Andrew Yang]

If you already know that the extension is galois then docs#exists_root_adjoin_eq_top_of_isCyclic works.
If not then docs#Field.powerBasisOfFiniteOfSeparable gives a generator with a deg 2 monic minimal polynomial and you can just shift the generator. We don't have this in mathlib IIRC and it would be nice to have.

[Ludwig Monnerjahn]

Thanks, my extension is Galois, but I will try to prove the second one.

[Andrew Yang]

Or maybe a better way is to show that every deg 2 extension is normal.