Theorems · Theorem · number theory

IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two

∀ (n : ℕ) [NeZero n] (K : Type u) [inst : Field K] [inst_1 : CharZero K] [h : IsCyclotomicExtension {n} ℚ K],
  NumberField.InfinitePlace.nrComplexPlaces K = n.totient / 2

If K is an 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.

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings

Cited by

4 results in Mathlib

Foundations

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

Assumes

NeZeroFieldCharZeroIsCyclotomicExtension