infinitePlace — Mathlib

English

If there exists a primitive root of unity of order k > 2 in K, then nrRealPlaces(K) = 0.

Русский

Если в K существует примитивный корень порядка k>2, то nrRealPlaces(K) = 0.

LaTeX

$$$(\exists \zeta, k)(2 < k \wedge IsPrimitiveRoot(\zeta,k)) \Rightarrow \operatorname{nrRealPlaces}(K) = 0$$$

Lean4

/-- The infinite place of `ℚ`, coming from the canonical map `ℚ → ℂ`. -/
noncomputable def infinitePlace : InfinitePlace ℚ :=
  .mk (Rat.castHom _)

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