Mathlib Map

Theorems · Inductive type · group theory

IsZGroup

(G : Type u_1) → [Group G] → Prop

A Z-group is a group whose Sylow subgroups are all cyclic.

Defined in
Mathlib.GroupTheory.SpecificGroups.ZGroup
Cited by
12 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

isZGroup_iff · cited by 2isZGroup_iffIsPGroup.isCyclic_of_isZGroup · cited by 1IsPGroup.isCyclic_of_isZG…IsZGroup.casesOn · cited by 1IsZGroup.casesOnIsZGroup.coprime_commutator_index · cited by 1IsZGroup.coprime_commutat…IsZGroup.isCyclic_commutator · cited by 1IsZGroup.isCyclic_commuta…IsZGroup.isZGroup · cited by 1IsZGroup.isZGroupisZGroup_of_coprime · cited by 1isZGroup_of_coprimeIsZGroup.of_injective · cited by 1IsZGroup.of_injectiveIsZGroup.commutator_lt · cited by 0IsZGroup.commutator_ltIsZGroup.exponent_eq_card · cited by 0IsZGroup.exponent_eq_cardisZGroup_iff_exists_mulEquiv · cited by 0isZGroup_iff_exists_mulEq…IsZGroup.of_squarefree · cited by 0IsZGroup.of_squarefreeIsZGroup.of_surjective · cited by 0IsZGroup.of_surjectiveIsZGroup.recOn · cited by 0IsZGroup.recOnGroup · cited by 6238GroupIsZGroupCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Groupstatement · cited by 6,238

Cited by14

Results whose statement or proof uses this declaration.