Quadratic algebras as number fields

A rational quadratic algebra whose defining polynomial has no rational root is a number field. The nonsquare hypothesis for an integer parameter transfers to its rational cast, and holds automatically for a negative integer parameter.

instance Int.instFactNotIsSquareNegNatCast (n : ℕ) [NeZero n] : Fact ¬IsSquare (-↑n)

A negative integer is not a square.

instance Rat.instFactNotIsSquareIntCast (D : ℤ) [Fact ¬IsSquare D] : Fact ¬IsSquare ↑D

A nonsquare integer remains nonsquare in the rationals.

instance QuadraticAlgebra.instNumberField {a b : ℚ} [Fact (∀ (r : ℚ), r ^ 2 ≠ a + b * r)] : NumberField (QuadraticAlgebra ℚ a b)

A rational quadratic algebra with no rational root is a number field.