to_noMaxOrder — Mathlib

English

In a cyclic linearly ordered group, two elements g1,g2 below 1 with the same zpowers must be equal.

Русский

В циклической линейно упорядоченной группе, если g1,g2 < 1 и zpowers(g1)=zpowers(g2), то g1=g2.

LaTeX

$$$(g_1<1) \land (g_2<1) \land (Subgroup.zpowers g_1)=(Subgroup.zpowers g_2) \Rightarrow g_1=g_2$$$

Lean4

@[to_additive]
instance (priority := 100) to_noMaxOrder [Nontrivial α] : NoMaxOrder α :=
  ⟨by
    obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'
    exact fun a => ⟨a * y, lt_mul_of_one_lt_right' a hy⟩⟩
    -- see Note [lower instance priority]

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