Theorems · Theorem · order theory

AddSubgroup.mem_closure_singleton_iff_existsUnique_zsmul

∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b : G},
  a ≠ 0 → (b ∈ AddSubgroup.closure {a} ↔ ∃! k, k • a = b)

The additive subgroup generated by an element of an additive group equals the set of integer multiples of the element, such that each multiple is a unique element. This is the stronger version of AddSubgroup.mem_closure_singleton.

Defined in

Mathlib.GroupTheory.ArchimedeanDensely

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoid