Cyclotomic extensions of ℚ are totally complex number fields.

We prove that cyclotomic extensions of ℚ are totally complex, meaning that NrRealPlaces K = 0 if IsCyclotomicExtension {n} ℚ K and 2 < n.

Main results

• nrRealPlaces_eq_zero: If K is a n-th cyclotomic extension of ℚ, where 2 < n, then there are no real places of K.

theorem IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero {n : ℕ} [NeZero n] (K : Type u) [Field K] [CharZero K] [IsCyclotomicExtension {n} ℚ K] (hn : 2 < n) : NumberField.InfinitePlace.nrRealPlaces K = 0

If K is a n-th cyclotomic extension of ℚ, where 2 < n, then there are no real places of K.

theorem IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two (n : ℕ) [NeZero n] (K : Type u) [Field K] [CharZero K] [h : IsCyclotomicExtension {n} ℚ K] : NumberField.InfinitePlace.nrComplexPlaces K = n.totient / 2

If K is a n-th cyclotomic extension of ℚ, then there are φ n / n complex places of K. Note that this uses 1 / 2 = 0 in the cases n = 1, 2.