multiplicative_int_orderMonoidIso_of_isLeast_one_lt

English

If there is a least positive element in a linearly ordered archimedean additive group G, then G is order-isomorphic (as an ordered group) to the integers.

Русский

Если в линейно упорядоченной архимедовой аддитивной группе G существует наименьший положительный элемент, то G изоморфна как упорядоченная группа целым числам.

LaTeX

$$$ \text{IsLeast}(\{ y>0 \}) \Rightarrow G \cong_o \mathbb{Z}. $$$

Lean4

/-- If an element of a linearly ordered mul-archimedean group is the least element greater than 1,
then the whole group is isomorphic (and order-isomorphic) to the multiplicative integers. -/
noncomputable def multiplicative_int_orderMonoidIso_of_isLeast_one_lt {x : G} (h : IsLeast {y : G | 1 < y} x) :
    G ≃*o Multiplicative ℤ := by
  have : IsLeast {y : Additive G | 0 < y} (.ofMul x) := h
  let f' := LinearOrderedAddCommGroup.int_orderAddMonoidIso_of_isLeast_pos (G := Additive G) this
  exact f'.toMultiplicativeRight

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