English
If K is an n-th cyclotomic extension of ℚ, then the number of complex places equals φ(n)/2 (with the convention φ(1)=φ(2)=1 giving a zero adjustment).
Русский
Если K есть n-ое циклотомическое расширение над ℚ, то число комплексных мест равно φ(n)/2.
LaTeX
$$$\mathrm{nrComplexPlaces} \, K = \dfrac{\varphi(n)}{2}$$$
Lean4
/-- 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`. -/
theorem nrComplexPlaces_eq_totient_div_two [h : IsCyclotomicExtension { n } ℚ K] :
haveI := IsCyclotomicExtension.numberField { n } ℚ K
nrComplexPlaces K = φ n / 2 :=
by
have := IsCyclotomicExtension.numberField { n } ℚ K
by_cases hn : 2 < n
· obtain ⟨k, hk : φ n = k + k⟩ := totient_even hn
have key := card_add_two_mul_card_eq_rank K
rw [nrRealPlaces_eq_zero K hn, zero_add,
IsCyclotomicExtension.finrank (n := n) K (cyclotomic.irreducible_rat (NeZero.pos _)), hk, ← two_mul,
Nat.mul_right_inj (by simp)] at key
simp [hk, key, ← two_mul]
· have : φ n = 1 := by
by_cases h1 : 1 < n
· convert totient_two
exact (eq_of_le_of_not_lt (succ_le_of_lt h1) hn).symm
· convert totient_one
exact eq_of_le_of_not_lt (not_lt.mp h1) (by simp [NeZero.ne _])
rw [this]
apply nrComplexPlaces_eq_zero_of_finrank_eq_one
rw [IsCyclotomicExtension.finrank K (cyclotomic.irreducible_rat (NeZero.pos n)), this]
