Theorems · Definition · group theory
SubMulAction.ofStabilizer
(G : Type u_1) →
[inst : Group G] → {α : Type u_2} → [inst_1 : MulAction G α] → (a : α) → SubMulAction (↥(MulAction.stabilizer G a)) αAction of the stabilizer of a point on the complement.
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound
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 · cited by 3,593
- Compl.complproof · cited by 2,925
- MulActionstatement and proof · cited by 1,294
- MulAction.stabilizerstatement and proof · cited by 254
- SubMulActionstatement · cited by 120
Cited by38
Results whose statement or proof uses this declaration.
- SubMulAction.ofStabilizer.conjMapstatement and proof · cited by 6
- SubMulAction.ofStabilizer.isMultiplyPretransitivestatement and proof · cited by 5
- SubMulAction.ofStabilizer.snocstatement and proof · cited by 4
- SubMulAction.fixingSubgroupInsertEquivstatement and proof · cited by 3
- SubMulAction.ofFixingSubgroup_insert_map_bijectivestatement and proof · cited by 3
- MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_mulproof · cited by 2
- MulAction.IsPreprimitive.isMultiplyPreprimitiveproof · cited by 2
- MulAction.IsPreprimitive.is_two_motive_of_is_motiveproof · cited by 2
- SubMulAction.ofStabilizer.conjMap_bijectivestatement and proof · cited by 2
- SubMulAction.nat_card_ofStabilizer_add_one_eqstatement · cited by 2
- SubMulAction.ofFixingSubgroup_insert_mapstatement and proof · cited by 2
- MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizerstatement and proof · cited by 2