nrRealPlaces_eq_zero — Mathlib

English

If K is the n-th cyclotomic extension of the rationals with n > 2, then K has no real places. Equivalently nrRealPlaces(K) = 0.

Русский

Если K является n-ым циклотомическим расширением по отношению к ℚ и n > 2, то у K нет вещественных мест; то есть nrRealPlaces(K) = 0.

LaTeX

$$$\text{nrRealPlaces } K = 0$$$

Lean4

/-- If `K` is a `n`-th cyclotomic extension of `ℚ`, where `2 < n`, then there are no real places
of `K`. -/
theorem nrRealPlaces_eq_zero [IsCyclotomicExtension { n } ℚ K] (hn : 2 < n) :
    haveI := IsCyclotomicExtension.numberField { n } ℚ K
    nrRealPlaces K = 0 :=
  by
  have := IsCyclotomicExtension.numberField { n } ℚ K
  apply (IsCyclotomicExtension.zeta_spec n ℚ K).nrRealPlaces_eq_zero_of_two_lt hn

Похожие утверждения