The {1, x} rational basis of algebraic integers in a quadratic number field

Internal helper: in a quadratic number field K, an integral element x that is not rational packages the pair {1, x} as a ℚ-basis of K whose two vectors are algebraic integers. It is not claimed to be a ℤ-basis of the full ring of integers 𝓞 K. This construction is shared by the effective discriminant bound NumberField.abs_discr_le_of_sq_intCast and the roadmap's ℚ(i) discriminant worked example, so it lives in the generic NumberField.Internal namespace rather than being duplicated inline or exposed from either headline API file.

theorem NumberField.Internal.exists_basis_eq_one_self_of_notMem_range_of_isIntegral {K : Type u_1} [Field K] [NumberField K] {x : K} (hfin : Module.finrank ℚ K = 2) (hx : x ∉ (algebraMap ℚ K).range) (hxint : IsIntegral ℤ x) : ∃ (b : Module.Basis (Fin 2) ℚ K), ⇑b = ![1, x] ∧ ∀ (i : Fin 2), IsIntegral ℤ (b i)

In a quadratic number field, an integral non-rational element x gives the ℚ-basis {1, x} of algebraic integers.