to_noMinOrder — Mathlib

English

In a linearly ordered cyclic group, if g<1 and zpowers g equals the top subgroup, then g is the LTOne generator of the top subgroup.

Русский

В линейно упорядоченной циклической группе, если g<1 и zpowers(g)=⊤, то g есть LTOne-порождающий верхней подгруппы.

LaTeX

$$$g<1 \land Subgroup.zpowers g = \top \Rightarrow g = (\top).genLTOne$$$

Lean4

@[to_additive]
instance (priority := 100) to_noMinOrder [Nontrivial α] : NoMinOrder α :=
  ⟨by
    obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'
    exact fun a => ⟨a / y, (div_lt_self_iff a).mpr hy⟩⟩

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