algebraic extensions of \R

Stream: Is there code for X?

[Francesco Minnocci]

Is there code for saying that the only non-trivial algebraic field extension of $\mathbb{R}$ is $\mathbb{C}$?

[Riccardo Brasca]

We have docs#Irreducible.degree_le_two that is more or less what you want

[Riccardo Brasca]

(the name should be changed to something containing real)

[Francesco Minnocci]

Riccardo Brasca said:

We have docs#Irreducible.degree_le_two that is more or less what you want

okay I'll try starting from that. On another note, do you know if there is code relating Algebra.adjoin withIntermediateField.adjoin? More specifically, I'm adjoining an algebraic element of a division algebra to the base field through Algebra.adjoin, but the resulting algebra is a field (since the element is algebraic); do I need to prove it by hand or is it somewhere in mathlib?

[Riccardo Brasca]

It is surely there, look around IntermediateField, that is probably better than Algebra.adjoin

[Riccardo Brasca]

Not sure it works for noncommutative stuff though