Theorems · Theorem · group theory
QuotientGroup.leftRel_apply
∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {x y : α}, (QuotientGroup.leftRel s) x y ↔ x⁻¹ * y ∈ s- Defined in
- Mathlib.GroupTheory.Coset.Defs
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 67 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.
Cites6
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
- Equiv.symmproof · cited by 3,681
- Subgroupstatement and proof · cited by 3,593
- QuotientGroup.leftRelstatement · cited by 61
- Equiv.exists_congr_leftproof · cited by 33
- Subgroup.equivOpproof · cited by 4
Cited by17
Results whose statement or proof uses this declaration.
- QuotientGroup.eqproof · cited by 20
- QuotientGroup.kerLift_injectiveproof · cited by 3
- Subgroup.IsComplement.inv_toLeftFun_mul_memproof · cited by 3
- CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroupproof · cited by 1
- QuotientGroup.leftRel_eqproof · cited by 1
- MulAction.injective_ofQuotientStabilizerproof · cited by 1
- Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroupOpproof · cited by 1
- DoubleCoset.bot_rel_eq_leftRelproof · cited by 1
- ModularGroup.exists_bound_of_subgroup_invariant_of_isBigOproof · cited by 1
- groupCohomology.H1InfRes_exactproof · cited by 0
- Subgroup.isQuotientCoveringMapproof · cited by 0
- Subgroup.isQuotientCoveringMap_of_commproof · cited by 0