exists_generator_lt_one — Mathlib

English

From a cone in a commutative group, one obtains an ordered monoid structure on the group; left-multiplication preserves order.

Русский

Из конуса в коммутативной группе получается упорядоченная структура моноида; левое умножение сохраняет порядок.

LaTeX

$$$\forall S,G,\ [Group G], [CommGroup G], [SetLike S G], (C:S) \Rightarrow IsOrderedMonoid G$ с соответствующим определением mul_le_mul_left.$$

Lean4

@[to_additive exists_neg_generator]
theorem exists_generator_lt_one : ∃ (a : G), a < 1 ∧ Subgroup.zpowers a = H :=
  by
  obtain ⟨a, ha⟩ := H.isCyclic_iff_exists_zpowers_eq_top.mp hH
  obtain ha1 | rfl | ha1 := lt_trichotomy a 1
  · exact ⟨a, ha1, ha⟩
  · rw [Subgroup.zpowers_one_eq_bot] at ha
    exact absurd ha.symm <| (H.nontrivial_iff_ne_bot).mp inferInstance
  · use a⁻¹, Left.inv_lt_one_iff.mpr ha1
    rw [Subgroup.zpowers_inv, ha]

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