Algebraic numbers

Stream: Is there code for X?

[Alfredo Moreira-Rosa]

Have algebraic numbers ℚ̅ been already defined in Mathlib ? With Coe ℚ̅ ℝ ? if so is there any pointers to the definition ? can't seem to find it.

[Riccardo Brasca]

Algebraic numbers are simply integralClosure ℚ ℂ (you may want to use IsIntegralClosure depending on what you need to do). What do you mean by a coercion to ℝ? There are algebraic numbers that are not real.

[Riccardo Brasca]

Or you may use docs#AlgebraicClosure

[Riccardo Brasca]

again, it depends on what you are doing

[Alfredo Moreira-Rosa]

yes, i'm particularly looking for algebraic real numbers, sorry

[Riccardo Brasca]

integralClosure ℚ ℝ is a subalgebra of ℝ, so it is probably what you need

[Riccardo Brasca]

but a more idiomatic way is probably something like K with isIntegralClosure K ℚ ℝ

[Riccardo Brasca]

so you work with "any" ring that is abstractly the field of real algebraic numbers, not the actual subset of the reals

[Alfredo Moreira-Rosa]

Thank you very much !