Theorems · Definition · group theory

SubMulAction.fixingSubgroupInsertEquiv

{M : Type u_1} →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] →
        (a : α) →
          (s : Set ↥(SubMulAction.ofStabilizer M a)) →
            ↥(fixingSubgroup M (insert a (Subtype.val '' s))) ≃* ↥(fixingSubgroup (↥(MulAction.stabilizer M a)) s)

The natural group isomorphism between fixing subgroups.

Defined in: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Cited by: 3 results in Mathlib
Foundations: Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Group MulAction

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Groupstatement and proof · cited by 6,238
Set.imagestatement and proof · cited by 5,609
Subgroupstatement · cited by 3,593
MulActionstatement and proof · cited by 1,294
MulEquivstatement · cited by 1,142
MulAction.stabilizerstatement and proof · cited by 254
SubMulActionstatement · cited by 120
fixingSubgroupstatement and proof · cited by 83
SubMulAction.ofStabilizerstatement and proof · cited by 33

Cited by4

Results whose statement or proof uses this declaration.

SubMulAction.ofFixingSubgroup_insert_map_bijectivestatement · cited by 3
SubMulAction.ofFixingSubgroup_insert_mapstatement · cited by 2
MulAction.isPreprimitive_fixingSubgroup_insert_iffproof · cited by 1
SubMulAction.ofFixingSubgroup_insert_map_applystatement · cited by 0