instance QuadraticAlgebra.instIsQuadraticExtension (a b : ℚ) [Fact (∀ (r : ℚ), r ^ 2 ≠ a + b * r)] : Algebra.IsQuadraticExtension ℚ (QuadraticAlgebra ℚ a b)

Any QuadraticAlgebra ℚ a b that is a field is automatically a quadratic extension of ℚ, i.e., a degree-2 extension. Combined with IsQuadraticField.instNumberField, this gives NumberField (QuadraticAlgebra ℚ a b) for free.

instance Algebra.IsQuadraticExtension.to_numberField (K : Type u_1) [Field K] [CharZero K] [IsQuadraticExtension ℚ K] : NumberField K

A quadratic field is a number field: it has characteristic zero and is finite-dimensional over ℚ.