English
If K contains a primitive k-th root of unity with k > 2, then K has no real places; i.e., nrRealPlaces(K) = 0.
Русский
Если K содержит примитивный корень порядка k > 2, то действительных мест нет; т.е. nrRealPlaces(K) = 0.
LaTeX
$$$(\exists \zeta \in K)(\exists k>2)(IsPrimitiveRoot(\zeta,k)) \Rightarrow \operatorname{nrRealPlaces}(K) = 0$$$
Lean4
theorem nrRealPlaces_eq_zero_of_two_lt (hk : 2 < k) (hζ : IsPrimitiveRoot ζ k) :
NumberField.InfinitePlace.nrRealPlaces K = 0 :=
by
refine (@Fintype.card_eq_zero_iff _ (_)).2 ⟨fun ⟨w, hwreal⟩ ↦ ?_⟩
rw [NumberField.InfinitePlace.isReal_iff] at hwreal
let f := w.embedding
have hζ' : IsPrimitiveRoot (f ζ) k := hζ.map_of_injective f.injective
have him : (f ζ).im = 0 :=
by
rw [← Complex.conj_eq_iff_im, ← NumberField.ComplexEmbedding.conjugate_coe_eq]
congr
have hre : (f ζ).re = 1 ∨ (f ζ).re = -1 :=
by
rw [← Complex.abs_re_eq_norm] at him
have := Complex.norm_eq_one_of_pow_eq_one hζ'.pow_eq_one (by cutsat)
rwa [← him, ← abs_one, abs_eq_abs] at this
cases hre with
| inl hone => exact hζ'.ne_one (by cutsat) <| Complex.ext (by simp [hone]) (by simp [him])
| inr hnegone =>
replace hζ' := hζ'.eq_orderOf
simp only [show f ζ = -1 from Complex.ext (by simp [hnegone]) (by simp [him]), orderOf_neg_one, ringChar.eq_zero,
OfNat.zero_ne_ofNat, ↓reduceIte] at hζ'
cutsat
