Theorems · Theorem · group theory
mem_leftCoset_iff
∀ {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ a • s ↔ a⁻¹ * x ∈ s- Defined in
- Mathlib.GroupTheory.Coset.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Groupstatement and proof · cited by 6,238
- Set.smulSetstatement · cited by 608
- inv_mul_cancel_leftproof · cited by 88
- mul_inv_cancel_leftproof · cited by 86
Cited by6
Results whose statement or proof uses this declaration.
- Subgroup.exists_finiteIndex_of_leftCoset_cover_auxproof · cited by 2
- Subgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eqproof · cited by 1
- CategoryTheory.PreGaloisCategory.toAut_surjective_of_isPretransitiveproof · cited by 1
- MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isEverywherePosproof · cited by 1
- QuotientGroup.eq_class_eq_leftCosetproof · cited by 0
- NonarchimedeanGroup.exists_openSubgroup_separatingproof · cited by 0