mem_torsion — Mathlib

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]⟩

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