English
If the Q-rank is 1, then nrComplexPlaces K = 0.
Русский
Если ранг над \mathbb{Q} равен 1, то nrComplexPlaces K = 0.
LaTeX
$$finrank_{\mathbb{Q}} K = 1 \Rightarrow nrComplexPlaces(K) = 0$$
Lean4
theorem mem_torsion {x : (𝓞 K)ˣ} : x ∈ torsion K ↔ ∀ w : InfinitePlace K, w x = 1 :=
by
rw [eq_iff_eq (x : K) 1, torsion, CommGroup.mem_torsion]
refine
⟨fun hx φ ↦ (((φ.comp <| algebraMap (𝓞 K) K).toMonoidHom.comp <| Units.coeHom _).isOfFinOrder hx).norm_eq_one,
fun h ↦ isOfFinOrder_iff_pow_eq_one.2 ?_⟩
obtain ⟨n, hn, hx⟩ := Embeddings.pow_eq_one_of_norm_eq_one K ℂ x.val.isIntegral_coe h
exact
⟨n, hn, by ext;
rw [NumberField.RingOfIntegers.coe_eq_algebraMap, coe_pow, hx, NumberField.RingOfIntegers.coe_eq_algebraMap,
coe_one]⟩