Theorems · Definition · group theory
SubAddAction.ofStabilizer
(G : Type u_1) →
[inst : AddGroup G] →
{α : Type u_2} → [inst_1 : AddAction G α] → (a : α) → SubAddAction (↥(AddAction.stabilizer G a)) αAction of the stabilizer of a point on the complement.
- Cited by
- 29 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.
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement · cited by 3,232
- Compl.complproof · cited by 2,925
- AddActionstatement and proof · cited by 820
- AddAction.stabilizerstatement and proof · cited by 112
- SubAddActionstatement · cited by 86
Cited by34
Results whose statement or proof uses this declaration.
- SubAddAction.ofStabilizer.conjMapstatement and proof · cited by 6
- SubAddAction.ofStabilizer.snocstatement and proof · cited by 4
- SubAddAction.fixingAddSubgroupInsertEquivstatement and proof · cited by 3
- SubAddAction.mem_ofStabilizer_iffstatement · cited by 3
- SubAddAction.ofFixingAddSubgroup_insert_mapstatement and proof · cited by 2
- SubAddAction.ofFixingAddSubgroup_insert_map_bijectivestatement and proof · cited by 2
- SubAddAction.ofStabilizer.addConjMap_bijectivestatement and proof · cited by 2
- SubAddAction.ofStabilizer.isMultiplyPretransitivestatement and proof · cited by 2
- SubAddAction.exists_vadd_of_last_eqstatement and proof · cited by 1
- AddAction.isMultiplyPreprimitive_ofStabilizerstatement and proof · cited by 1
- AddAction.isPreprimitive_fixingAddSubgroup_insert_iffstatement and proof · cited by 1
- SubAddAction.mem_ofFixingAddSubgroup_insert_iffstatement and proof · cited by 1