adjoin finset is number field

Stream: Is there code for X?

[Andrew Yang]

How would one go and prove?

import number_theory.number_field

example (x y : ℂ) : number_field (intermediate_field.adjoin ℚ ({x, y} : set ℂ)) := sorry

I couldn't find the relavent lemmas regarding finite dimensionality, and there seems to be a diamond between the module ℚ _ instance induced from the intermediate_field and the char_zero.

[Damiano Testa]

I haven't played with the API, but I suspect some assumption is missing: what if x = π?

[Andrew Yang]

Oops I have modified the type signature. Thanks.

[Andrew Yang]

For some context, I am defining bezout domains to work with valuation rings, and I thought it would be nice if I could show that the ring of algebraic integers is bezout.

[Junyan Xu]

I think you can just use docs#fg_adjoin_of_finite since finite_dimensional in the definition of docs#number_field is just an abbreviation for docs#module.finite which is defined to mean the top submodule is fg.

[Andrew Yang]

Do we know that intermediate_field.adjoin coincides with algebra.adjoin when the elements adjoined are all algebraic?

[Junyan Xu]

I could only find docs#intermediate_field.adjoin_simple_to_subalgebra_of_integral for adjoining one (algebraic, stated as is_integral) element. Hopefully it's not hard to use induction to get the full result.