Theorems · Theorem · group theory
Subgroup.pow_index_mem
∀ {G : Type u_6} [inst : Group G] (H : Subgroup G) [H.Normal] (g : G), g ^ H.index ∈ H- Defined in
- Mathlib.GroupTheory.OrderOfElement
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupSubgroup.Normal
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.
- Groupstatement and proof · cited by 6,238
- Subgroupstatement and proof · cited by 3,593
- HasQuotient.Quotientproof · cited by 2,301
- Subgroup.Normalstatement and proof · cited by 334
- QuotientGroup.mkproof · cited by 196
- Subgroup.indexstatement and proof · cited by 150
- QuotientGroup.eq_one_iffproof · cited by 18
- pow_card_eq_one'proof · cited by 9
- QuotientGroup.mk_powproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- Subgroup.pow_relIndex_memproof · cited by 0
- MonoidHom.transfer_center_eq_powstatement · cited by 0