Theorems · Definition · group theory
AddAction.orbitEquivQuotientStabilizer
(G : Type u) →
{X : Type v} →
[inst : AddGroup G] → [inst_1 : AddAction G X] → (b : X) → ↑(AddAction.orbit G b) ≃ G ⧸ AddAction.stabilizer G bOrbit-stabilizer theorem.
- Defined in
- Mathlib.GroupTheory.GroupAction.Quotient
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- Set.Elemstatement · cited by 7,166
- AddGroupstatement and proof · cited by 4,410
- Equiv.symmproof · cited by 3,681
- AddSubgroupstatement · cited by 3,232
- HasQuotient.Quotientstatement and proof · cited by 2,301
- AddActionstatement and proof · cited by 820
- AddAction.stabilizerstatement and proof · cited by 112
- AddAction.orbitstatement · cited by 86
- Equiv.ofBijectiveproof · cited by 70
- AddAction.ofQuotientStabilizerproof · cited by 4
- AddAction.ofQuotientStabilizer_mem_orbitproof · cited by 0
Cited by5
Results whose statement or proof uses this declaration.
- AddAction.orbitZMultiplesEquivproof · cited by 4
- AddAction.index_stabilizerproof · cited by 3
- AddAction.selfEquivSigmaOrbitsQuotientStabilizer'proof · cited by 1
- AddAction.orbitProdStabilizerEquivAddGroupproof · cited by 1
- AddAction.orbitEquivQuotientStabilizer_symm_applystatement · cited by 0