The field ℚ(√2)

Let K be a number field generated over ℚ by an algebraic integer θ with minpoly ℤ θ = X² − 2, that is K = ℚ(√2). This file records the basic shape of this presentation, shared by the worked examples: θ² = 2 and [K : ℚ] = 2.

Main results

• TauCeti.NumberField.Sqrt2.sq_eq_two: θ² = 2.
• TauCeti.NumberField.Sqrt2.finrank_eq_two: [K : ℚ] = 2.

@[simp]

theorem TauCeti.NumberField.Sqrt2.sq_eq_two {K : Type u_1} [Field K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) : θ ^ 2 = 2

The defining identity θ² = 2.

theorem TauCeti.NumberField.Sqrt2.finrank_eq_two {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) (hgen : ℚ[↑θ] = ⊤) : Module.finrank ℚ K = 2

ℚ(√2) has degree 2.