Mathlib Map

Theorems · Definition · group theory

IsPGroup

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

A p-group is a group in which the order of every element is a power of p.

Defined in
Mathlib.GroupTheory.PGroup
Cited by
96 results in Mathlib
Foundations
Depth 19 from the axioms, rests on 139 definitions · uses propext
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Sylow.isPGroup' · cited by 19Sylow.isPGroup'IsPGroup.iff_card · cited by 7IsPGroup.iff_cardSylow.is_maximal' · cited by 6Sylow.is_maximal'IsPGroup.exists_card_eq · cited by 5IsPGroup.exists_card_eqIsPGroup.of_card · cited by 5IsPGroup.of_cardIsPGroup.to_le · cited by 5IsPGroup.to_leIsPGroup.card_modEq_card_fixedPoints · cited by 4IsPGroup.card_modEq_card_…IsPGroup.map · cited by 4IsPGroup.mapIsPGroup.powEquiv' · cited by 4IsPGroup.powEquiv'IsPGroup.to_quotient · cited by 4IsPGroup.to_quotientIsPGroup.comap_of_ker_isPGroup · cited by 3IsPGroup.comap_of_ker_isP…IsPGroup.ker_isPGroup_of_injective · cited by 3IsPGroup.ker_isPGroup_of_…IsPGroup.of_surjective · cited by 3IsPGroup.of_surjectiveIsPGroup.toSylow · cited by 3IsPGroup.toSylowisPGroup_iff_orderOf_dvd_pow · cited by 3isPGroup_iff_orderOf_dvd_…Group · cited by 6238GroupIsPGroupCITED BYCITES

Cites1

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

Cited by105

Results whose statement or proof uses this declaration.