Theorems · Theorem · group theory
ZModModule.isPGroup_multiplicative
∀ {n : ℕ} {G : Type u_2} [inst : AddCommGroup G] [Module (ZMod n) G], IsPGroup n (Multiplicative G)- Defined in
- Mathlib.GroupTheory.PGroup
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 61 from the axioms · uses propext, Quot.sound
- Assumes
- AddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- ZModstatement and proof · cited by 1,024
- pow_oneproof · cited by 894
- Multiplicativestatement · cited by 875
- Multiplicative.ofAddproof · cited by 237
- IsPGroupstatement · cited by 96
- ZModModule.char_nsmul_eq_zeroproof · cited by 4
Cited by1
Results whose statement or proof uses this declaration.
- ZModModule.exists_submodule_subset_card_leproof · cited by 0