Theorems · Inductive type · group theory
IsAddCyclic
(G : Type u) → [SMul ℤ G] → Prop
A group is called cyclic if it is generated by a single element. [Wikidata Q245462](https://www.wikidata.org/wiki/Q245462)
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 55 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- SMul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by65
Results whose statement or proof uses this declaration.
- IsAddCyclic.exists_generatorstatement and proof · cited by 8
- IsAddCyclic.exponent_eq_cardstatement and proof · cited by 5
- isAddCyclic_of_surjectivestatement and proof · cited by 5
- AddEquiv.isAddCyclicstatement and proof · cited by 4
- AddSubgroup.isAddCyclic_iff_exists_zmultiples_eq_topstatement · cited by 4
- isAddCyclic_iff_exists_zmultiples_eq_topstatement and proof · cited by 4
- LinearOrderedAddCommGroup.Subgroup.negGenstatement and proof · cited by 3
- IsAddCyclic.casesOnstatement and proof · cited by 3
- IsAddCyclic.exists_zsmul_surjectivestatement and proof · cited by 3
- isAddCyclic_additive_iffstatement and proof · cited by 3
- isAddCyclic_of_addOrderOf_eq_cardstatement · cited by 3
- LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_intstatement and proof · cited by 2