The infinite places of a quadratic field ℚ(√d)

The signature of ℚ(√d) is read off the sign of d: for d < 0 the field is totally complex and for 0 ≤ d it is totally real. Both are special cases of the generic square-root criteria NumberField.isTotallyComplex_of_sq_ratCast_of_neg and NumberField.isTotallyReal_of_sq_ratCast_of_nonneg, applied to the generator θ with θ² = d. Total reality needs the generator hypothesis as well, since a real square root only forces the embeddings fixed on ℚ(θ) to be real.

Main results

• NumberField.isTotallyComplex_of_minpoly_eq_X_sq_sub_C_of_neg.
• NumberField.isTotallyReal_of_minpoly_eq_X_sq_sub_C_of_nonneg.

theorem NumberField.isTotallyComplex_of_minpoly_eq_X_sq_sub_C_of_neg {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hd : d < 0) : IsTotallyComplex K

An imaginary quadratic field is totally complex. Any number field K containing an algebraic integer θ with minpoly ℤ θ = X² - d and d < 0 is totally complex — in particular the imaginary quadratic field ℚ(√d).

theorem NumberField.isTotallyReal_of_minpoly_eq_X_sq_sub_C_of_nonneg {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hd : 0 ≤ d) : IsTotallyReal K

A real quadratic field is totally real. A number field K generated over ℚ by an algebraic integer θ with minpoly ℤ θ = X² - d and 0 ≤ d is totally real — in particular the real quadratic field ℚ(√d).