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