Theorems · Theorem · group theory
Subgroup.mul_mem_iff_of_index_two
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 2 → ∀ {a b : G}, a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)- Defined in
- Mathlib.GroupTheory.Index
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Group
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
- mul_assocproof · cited by 1,667
- Subgroup.indexstatement and proof · cited by 150
- Xorproof · cited by 56
- mul_mem_cancel_rightproof · cited by 11
- mul_mem_cancel_leftproof · cited by 10
- Xor.orproof · cited by 7
- Subgroup.index_eq_two_iffproof · cited by 4
Cited by3
Results whose statement or proof uses this declaration.
- Subgroup.normal_of_index_eq_twoproof · cited by 2
- Subgroup.mul_self_mem_of_index_twoproof · cited by 1
- Equiv.Perm.eq_alternatingGroup_of_index_eq_twoproof · cited by 1