mulArchimedean_iff — Mathlib

English

For a linear ordered group, Archimedean property holds for the unit group if and only if it holds for the original group.

Русский

Для линейно упорядоченной группы свойство Архимедова сохраняется в группе единиц, и наоборот.

LaTeX

$$$\mathrm{MulArchimedean}(G) \iff \mathrm{MulArchimedean}(G_{\mathrm{Units}})$$$

Lean4

theorem mulArchimedean_iff {G₀} [LinearOrderedCommGroupWithZero G₀] : MulArchimedean G₀ˣ ↔ MulArchimedean G₀ :=
  by
  constructor <;> intro _
  · exact OrderMonoidIso.withZeroUnits.mulArchimedean
  · infer_instance

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