Documentation

Mathlib.Algebra.Order.Group.Cyclic

Cyclic linearly ordered groups #

This file contains basic results about cyclic linearly ordered groups and cyclic subgroups of linearly ordered groups.

The definitions LinearOrderedCommGroup.Subgroup.genLTOne (resp. LinearOrderedCommGroup.genLTOone) yields a generator of a non-trivial subgroup of a linearly ordered commutative group with (resp. of a non-trivial linearly ordered commutative group) that is strictly less than 1. The corresponding additive definitions are also provided.

source
theorem LinearOrderedCommGroup.Subgroup.exists_generator_lt_one {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (H : Subgroup G) [Nontrivial ↥H] [hH : IsCyclic ↥H] :
∃ a < 1, Subgroup.zpowers a = H
source
theorem LinearOrderedAddCommGroup.Subgroup.exists_neg_generator {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (H : AddSubgroup G) [Nontrivial ↥H] [hH : IsAddCyclic ↥H] :
∃ a < 0, AddSubgroup.zmultiples a = H
source
noncomputable def LinearOrderedCommGroup.Subgroup.genLTOne {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (H : Subgroup G) [Nontrivial ↥H] [hH : IsCyclic ↥H] :
G

Given a subgroup of a cyclic linearly ordered commutative group, this is a generator of the subgroup that is < 1.

Equations
Instances For
    source
    noncomputable def LinearOrderedAddCommGroup.Subgroup.negGen {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (H : AddSubgroup G) [Nontrivial ↥H] [hH : IsAddCyclic ↥H] :
    G

    Given an additive subgroup of an additive cyclic linearly ordered commutative group, this is a negative generator of the subgroup.

    Equations
    Instances For
      source
      theorem LinearOrderedCommGroup.Subgroup.genLTOne_lt_one {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (H : Subgroup G) [Nontrivial ↥H] [hH : IsCyclic ↥H] :
      Subgroup.genLTOne H < 1
      source
      theorem LinearOrderedAddCommGroup.Subgroup.negGen_neg {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (H : AddSubgroup G) [Nontrivial ↥H] [hH : IsAddCyclic ↥H] :
      Subgroup.negGen H < 0
      source
      @[simp]
      theorem LinearOrderedCommGroup.Subgroup.genLTOne_zpowers_eq_top {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (H : Subgroup G) [Nontrivial ↥H] [hH : IsCyclic ↥H] :
      Subgroup.zpowers (Subgroup.genLTOne H) = H
      source
      @[simp]
      theorem LinearOrderedAddCommGroup.Subgroup.negGen_zmultiples_eq_top {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (H : AddSubgroup G) [Nontrivial ↥H] [hH : IsAddCyclic ↥H] :
      AddSubgroup.zmultiples (Subgroup.negGen H) = H
      source
      theorem LinearOrderedCommGroup.Subgroup.genLTOne_mem {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (H : Subgroup G) [Nontrivial ↥H] [hH : IsCyclic ↥H] :
      Subgroup.genLTOne H ∈ H
      source
      theorem LinearOrderedCommGroup.Subgroup.genLTOne_unique {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (H : Subgroup G) [Nontrivial ↥H] [hH : IsCyclic ↥H] {g : G} (hg : g < 1) :
      Subgroup.zpowers g = H → g = Subgroup.genLTOne H
      source
      theorem LinearOrderedCommGroup.Subgroup.genLTOne_unique_of_zpowers_eq {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {g1 g2 : G} (hg1 : g1 < 1) (hg2 : g2 < 1) (h : Subgroup.zpowers g1 = Subgroup.zpowers g2) :
      g1 = g2
      source
      noncomputable def LinearOrderedCommGroup.genLTOne (G : Type u_1) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] [IsCyclic G] :
      G

      Given a cyclic linearly ordered commutative group, this is a generator that is < 1.

      Equations
      Instances For
        source
        noncomputable def LinearOrderedAddCommGroup.negGen (G : Type u_1) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Nontrivial G] [IsAddCyclic G] :
        G

        Given an additive cyclic linearly ordered commutative group, this is a negative generator of it.

        Equations
        Instances For
          source
          @[simp]
          theorem LinearOrderedCommGroup.genLTOne_eq_of_top (G : Type u_1) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] [IsCyclic G] :
          genLTOne G = Subgroup.genLTOne ⊤
          source
          @[simp]
          theorem LinearOrderedAddCommGroup.negGen_eq_of_top (G : Type u_1) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Nontrivial G] [IsAddCyclic G] :
          negGen G = Subgroup.negGen ⊤
          source
          theorem LinearOrderedCommGroup.genLTOne_unique (G : Type u_1) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] [IsCyclic G] {g : G} (hg : g < 1) (htop : Subgroup.zpowers g = ⊤) :
          g = genLTOne G