Theorems · Theorem · group theory
IsCyclic.exists_generator
∀ {α : Type u_1} [inst : Group α] [IsCyclic α], ∃ g, ∀ (x : α), x ∈ Subgroup.zpowers g- Cited by
- 14 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- Subgroupstatement · cited by 3,593
- Subgroup.zpowersstatement · cited by 204
- IsCyclicstatement and proof · cited by 122
- exists_zpow_surjectiveproof · cited by 3
Cited by14
Results whose statement or proof uses this declaration.
- IsSimpleGroup.prime_cardproof · cited by 3
- MonoidHom.map_cyclicproof · cited by 3
- IsCyclic.exists_ofOrder_eq_natCardproof · cited by 3
- FiniteField.unit_isSquare_iffproof · cited by 2
- IsCyclic.card_pow_eq_one_leproof · cited by 2
- IsCyclic.extproof · cited by 1
- MonoidHom.isMulCommutative_of_isCyclic_of_ker_le_centerproof · cited by 1
- Field.exists_primitive_element_of_finite_topproof · cited by 1
- IsCyclic.monoidHom_mulEquiv_rootsOfUnityproof · cited by 1
- FiniteField.forall_pow_eq_one_iffproof · cited by 1
- reverse_lucas_primalityproof · cited by 1
- IsCyclic.exists_apply_ne_oneproof · cited by 1