The real places of ℚ(√2)

For K generated over ℚ by an algebraic integer θ with minpoly ℤ θ = X² − 2, the real number √2 is a root of X² − 2, so there is a real infinite place w of K coming from the real embedding sending θ to √2; at that place 1 + θ has absolute value 1 + √2. A real quadratic field has unit rank one.

Main results

• TauCeti.NumberField.Sqrt2.exists_isReal_and_apply_eq_one_add_sqrt_two: a real place where 1 + θ has absolute value 1 + √2.
• TauCeti.NumberField.Sqrt2.units_rank_eq_one: unit rank one.

theorem TauCeti.NumberField.Sqrt2.exists_isReal_and_apply_eq_one_add_sqrt_two {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) (hgen : ℚ[↑θ] = ⊤) : ∃ (w : NumberField.InfinitePlace K), w.IsReal ∧ w ↑(1 + θ) = 1 + √2

The real place at 1 + √2. There is a real infinite place w of ℚ(√2) at which 1 + θ has absolute value w (1 + θ) = 1 + √2.

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

ℚ(√2) has unit rank one.