Theorems · Theorem · group theory

SubMulAction.fixingSubgroup_of_insert

∀ {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 ((fun x => ↑x) '' s)) =
    Subgroup.map (MulAction.stabilizer M a).subtype (fixingSubgroup (↥(MulAction.stabilizer M a)) s)

Defined in: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Cited by: 1 results in Mathlib
Foundations: Depth 26 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.

Cites13

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 · cited by 5,609
Subgroupstatement · cited by 3,593
MulActionstatement and proof · cited by 1,294
Subgroup.mapstatement · cited by 301
MulAction.stabilizerstatement and proof · cited by 254
Subgroup.subtypestatement · cited by 185
SubMulActionstatement · cited by 120
Subgroup.extproof · cited by 108
fixingSubgroupstatement · cited by 83
SMulMemClass.smul_memproof · cited by 55

Cited by1

Results whose statement or proof uses this declaration.

MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_mulproof · cited by 2