Theorems · Definition · group theory
AddAction.orbitRel.Quotient
(G : Type u_1) → (α : Type u_2) → [inst : AddGroup G] → [AddAction G α] → Type u_2
The quotient by AddAction.orbitRel, given a name to enable dot notation.
- Defined in
- Mathlib.GroupTheory.GroupAction.Defs
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- AddActionstatement and proof · cited by 820
- AddAction.orbitRelproof · cited by 47
Cited by23
Results whose statement or proof uses this declaration.
- AddAction.orbitRel.Quotient.orbitstatement and proof · cited by 15
- AddAction.orbitRel.Quotient.orbit_eq_orbit_outstatement and proof · cited by 4
- AddAction.pretransitive_iff_subsingleton_quotientstatement and proof · cited by 2
- AddAction.orbitRel.Quotient.mem_addSubgroup_orbit_iffstatement and proof · cited by 2
- AddAction.orbitRel.Quotient.mem_orbitstatement and proof · cited by 2
- AddAction.selfEquivSigmaOrbits'statement and proof · cited by 1
- AddAction.orbitRel.Quotient.orbit_injectivestatement and proof · cited by 1
- QuotientAddGroup.univ_eq_iUnion_vaddproof · cited by 1
- AddAction.orbitRel.Quotient.orbit.coe_vaddstatement and proof · cited by 1
- AddSubgroup.finite_quotient_of_finite_quotient_of_index_ne_zerostatement and proof · cited by 1
- AddAction.univ_eq_iUnion_orbitstatement and proof · cited by 1
- AddAction.pretransitive_iff_unique_quotient_of_nonemptystatement and proof · cited by 0