Theorems · Definition · group theory

Subgroup.zpowers

{G : Type u_1} → [inst : Group G] → G → Subgroup G

The subgroup generated by an element.

Defined in: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Cited by: 204 results in Mathlib
Foundations: Depth 32 from the axioms, rests on 245 definitions · uses propext
Assumes: Group

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites3

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
Set.rangeproof · cited by 4,705
Subgroupstatement · cited by 3,593

Cited by236

Results whose statement or proof uses this declaration.

Equiv.Perm.IsCycle.orderOfproof · cited by 14
IsCyclic.exists_generatorstatement · cited by 14
orderOf_eq_card_of_forall_mem_zpowersstatement and proof · cited by 13
Nat.card_zpowersstatement and proof · cited by 13
Subgroup.mem_zpowersstatement · cited by 12
Subgroup.zpowers_invstatement · cited by 11
intEquivOfZPowersEqTopstatement and proof · cited by 11
Subgroup.mem_zpowers_iffstatement · cited by 10
Equiv.Perm.OnCycleFactors.kerParamstatement · cited by 10
IsPrimitiveRoot.zmodEquivZPowersstatement · cited by 9
orderOf_dvd_cardproof · cited by 9
Equiv.Perm.pairwise_commute_of_mem_zpowersstatement and proof · cited by 7

Showing the 200 most cited of 236.