Theorems · Theorem · number theory

IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero

∀ {n : ℕ} [NeZero n] (K : Type u) [inst : Field K] [inst_1 : CharZero K] [inst_2 : IsCyclotomicExtension {n} ℚ K],
  2 < n → NumberField.InfinitePlace.nrRealPlaces K = 0

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

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings

Cited by

3 results in Mathlib

Foundations

Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NeZeroFieldCharZeroIsCyclotomicExtension