genLTOne — Mathlib

English

If zpowers(g) = H and g < 1, then g is the LTOne generator of H; equivalently, the unique g with zpowers g = H and g < 1 is H.genLTOne.

Русский

Если zpowers(g) = H и g < 1, то g является LTOne-генератором H; то есть единственное g с zpowers g = H и g < 1 есть H.genLTOne.

LaTeX

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

Lean4

/-- Given a cyclic linearly ordered commutative group, this is a generator that is `< 1`. -/
@[to_additive negGen /-- Given an additive cyclic linearly ordered commutative group, this is a
    negative generator of it. -/
    ]
noncomputable def genLTOne : G :=
  (⊤ : Subgroup G).genLTOne

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