Theorems · Theorem · group theory
QuotientGroup.eq
∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {a b : α}, ↑a = ↑b ↔ a⁻¹ * b ∈ s- Defined in
- Mathlib.GroupTheory.Coset.Defs
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 69 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
- Subgroupstatement and proof · cited by 3,593
- HasQuotient.Quotientstatement · cited by 2,301
- QuotientGroup.mkstatement · cited by 196
- Quotient.eq''proof · cited by 44
- QuotientGroup.leftRel_applyproof · cited by 17
Cited by20
Results whose statement or proof uses this declaration.
- QuotientGroup.eq_one_iffproof · cited by 18
- QuotientGroup.out_conj_pow_minimalPeriod_memproof · cited by 4
- QuotientGroup.mk_mul_of_memproof · cited by 2
- Subgroup.exists_pow_mem_of_index_ne_zeroproof · cited by 2
- QuotientGroup.eq_iff_div_memproof · cited by 2
- Subgroup.exists_finiteIndex_of_leftCoset_cover_auxproof · cited by 2
- QuotientGroup.mk'_eq_mk'proof · cited by 2
- IsGaloisGroup.quotientproof · cited by 1
- Subgroup.normalCore_eq_kerproof · cited by 1
- QuotientGroup.strictMono_comap_prod_imageproof · cited by 1
- QuotientGroup.subgroup_eq_top_of_subsingletonproof · cited by 1
- FixedPoints.toAlgAut_surjectiveproof · cited by 1