Theorems · Definition · group theory
fixingSubgroup
(M : Type u_1) → {α : Type u_2} → [inst : Group M] → [MulAction M α] → Set α → Subgroup MThe subgroup fixing a set under a MulAction.
- Cited by
- 83 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- Set.Elemproof · cited by 7,166
- Groupstatement and proof · cited by 6,238
- Subgroupstatement · cited by 3,593
- Submonoidproof · cited by 3,086
- MulActionstatement and proof · cited by 1,294
- Subsemigroup.carrierproof · cited by 160
- Submonoid.toSubsemigroupproof · cited by 159
- fixingSubmonoidproof · cited by 5
Cited by99
Results whose statement or proof uses this declaration.
- SubMulAction.ofFixingSubgroupstatement · cited by 43
- IntermediateField.fixingSubgroupproof · cited by 41
- mem_fixingSubgroup_iffstatement and proof · cited by 8
- fixingSubgroup_fixedPoints_gcstatement and proof · cited by 7
- MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroupstatement · cited by 6
- SubMulAction.fixingSubgroupEquivFixingSubgroupstatement and proof · cited by 5
- IsGaloisGroup.restrictHomproof · cited by 5
- MulAction.isMultiplyPreprimitive_iffstatement and proof · cited by 5
- SubMulAction.ofFixingSubgroup.appendstatement · cited by 4
- SubMulAction.ofFixingSubgroup.isMultiplyPretransitivestatement and proof · cited by 4
- SubMulAction.fixingSubgroupInsertEquivstatement and proof · cited by 3
- SubMulAction.ofFixingSubgroup_insert_map_bijectivestatement · cited by 3