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: IfKis an-th cyclotomic extension ofℚ, where2 < n, then there are no real places ofK.
theorem
IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero
{n : ℕ+}
(K : Type u)
[Field K]
[CharZero K]
[IsCyclotomicExtension {n} ℚ K]
(hn : 2 < n)
:
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 : ℕ+)
(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.