Int.subgroup_cyclic
theorem Int.subgroup_cyclic : ∀ (H : AddSubgroup ℤ), ∃ a, H = AddSubgroup.closure {a}
This theorem states that every subgroup of integers (`ℤ`) is cyclic. More specifically, it asserts that for every subgroup `H` of the integers, there exists an integer `a` such that `H` is the subgroup generated by `{a}`. This means that every element of `H` can be written as a sum or difference of copies of `a`, which is the formal definition of a cyclic group in group theory.
More concisely: Every subgroup of integers is cyclic, that is, for every subgroup H of ℤ, there exists an integer a such that H = {n : ℤ | n = mi for some i ∈ ℤ}.
|
AddSubgroup.cyclic_of_min
theorem AddSubgroup.cyclic_of_min :
∀ {G : Type u_1} [inst : LinearOrderedAddCommGroup G] [inst_1 : Archimedean G] {H : AddSubgroup G} {a : G},
IsLeast {g | g ∈ H ∧ 0 < g} a → H = AddSubgroup.closure {a}
The theorem `AddSubgroup.cyclic_of_min` states that for any subgroup `H` of a decidable linearly ordered archimedean abelian group `G`, if there exists a minimal element `a` in the intersection of `H` and the positive elements of `G`, then the subgroup `H` is generated by the element `a`. In simpler terms, if a smallest positive element exists in a subgroup of a certain type of group, then every element in this subgroup can be expressed as a multiple of this smallest positive element.
More concisely: If a subgroup of a decidable linearly ordered archimedean abelian group has a minimal positive element, then the subgroup is generated by that element.
|
AddSubgroup.cyclic_of_isolated_zero
theorem AddSubgroup.cyclic_of_isolated_zero :
∀ {G : Type u_1} [inst : LinearOrderedAddCommGroup G] [inst_1 : Archimedean G] {H : AddSubgroup G} {a : G},
0 < a → Disjoint (↑H) (Set.Ioo 0 a) → ∃ b, H = AddSubgroup.closure {b}
This theorem states that for a given additive subgroup of a linear ordered additive commutative group, if this subgroup is disjoint with the open interval from 0 to a positive number `a`, then this subgroup is a cyclic subgroup. In other words, there exists an element `b` such that this subgroup can be generated by recursively adding `b` to itself, expressed as `AddSubgroup.closure {b}` in Lean. This theorem holds under the condition that the underlying group is Archimedean, which is a property implying, among other things, that given any two positive group elements, there exists a positive integer multiple of the smaller element that exceeds the larger element.
More concisely: Given an additive subgroup of an Archimedean linear ordered additive commutative group that is disjoint with the open interval from 0 to a positive number, the subgroup is cyclic.
|
AddSubgroup.exists_isLeast_pos
theorem AddSubgroup.exists_isLeast_pos :
∀ {G : Type u_1} [inst : LinearOrderedAddCommGroup G] [inst_1 : Archimedean G] {H : AddSubgroup G},
H ≠ ⊥ → ∀ {a : G}, 0 < a → Disjoint (↑H) (Set.Ioo 0 a) → ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
The theorem `AddSubgroup.exists_isLeast_pos` states that if we have a nontrivial additive subgroup (`H ≠ ⊥`) of a linear ordered additive commutative group, such that this subgroup `H` and the interval from 0 to a positive number `a` (`Set.Ioo 0 a`) are disjoint, then there exists a least positive element in the subgroup `H`. In other words, among the positive elements of the subgroup, there is one that is smaller than all the others. Here, "least" is defined according to the order of the underlying group, and "positive" means greater than zero.
More concisely: If `H` is a nontrivial additive subgroup of a linear ordered additive commutative group disjoint from the interval `(0, a)`, then `H` contains a least positive element.
|