mulArchimedean_mrange_of_isCompact_integer

English

Under compactness of the valuation ring, the unit group of the range of the valuation admits a locally finite order.

Русский

При компактности кольца оценки допускается локально конечный порядок на группе единиц образа оценки.

LaTeX

$$$$ \text{If } 𝒪_K \text{ is compact, then } (\mathrm{mrange}(v))^{\times} \text{ has a LocallyFiniteOrder}. $$$$

Lean4

theorem mulArchimedean_mrange_of_isCompact_integer (hc : IsCompact (X := K) 𝒪[K]) :
    MulArchimedean (MonoidHom.mrange (Valued.v : Valuation K Γ₀)) :=
  by
  rw [← Units.mulArchimedean_iff]
  obtain ⟨_⟩ := locallyFiniteOrder_units_mrange_of_isCompact_integer hc
  exact MulArchimedean.of_locallyFiniteOrder

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