The field ℚ(i), presented by a square root of −1

Let K be a number field generated over ℚ by an algebraic integer θ with minpoly ℤ θ = X² + 1, that is K = ℚ(i) presented by a square root of −1. This file records the basic shape of this presentation, shared by the worked example: the defining identity θ² = −1, the minimal polynomial in the radicand form X² − C (−1) of the quadratic-field theory, and [K : ℚ] = 2.

Main results

• TauCeti.NumberField.GaussianRationals.sq_eq_neg_one: θ² = −1.
• TauCeti.NumberField.GaussianRationals.isUnit: θ is a unit, since θ · (−θ) = 1.
• TauCeti.NumberField.GaussianRationals.finrank_eq_two: [K : ℚ] = 2.

theorem TauCeti.NumberField.GaussianRationals.minpoly_eq_X_sq_sub_C {K : Type u_1} [Field K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C (-1)

The minimal polynomial X² + 1 in the radicand form X² − C (−1) of the quadratic-field theory.

@[simp]

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

The defining identity θ² = −1.

theorem TauCeti.NumberField.GaussianRationals.isUnit {K : Type u_1} [Field K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) : IsUnit θ

θ is a unit of 𝓞 K: θ · (−θ) = 1.

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

ℚ(i) has degree 2.