Theorems · Definition · group theory

LinearOrderedAddCommGroup.Subgroup.negGen

{G : Type u_1} →
  [inst : AddCommGroup G] →
    [inst_1 : 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.

Defined in

Mathlib.Algebra.Order.Group.Cyclic

Cited by

3 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidNontrivialIsAddCyclic