Theorems · Definition · group theory
MulAction.fixedPoints
(M : Type u_1) → (α : Type u_3) → [inst : Monoid M] → [MulAction M α] → Set α
The set of elements fixed under the whole action.
- Defined in
- Mathlib.GroupTheory.GroupAction.Defs
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Set.ofPredproof · cited by 6,101
- Monoidstatement and proof · cited by 3,887
- MulActionstatement and proof · cited by 1,294
Cited by51
Results whose statement or proof uses this declaration.
- FixedPoints.subfieldproof · cited by 20
- FixedPoints.intermediateFieldproof · cited by 18
- fixingSubgroup_fixedPoints_gcstatement and proof · cited by 7
- fixingSubmonoid_fixedPoints_gcstatement and proof · cited by 6
- IsPGroup.card_modEq_card_fixedPointsstatement and proof · cited by 4
- MulAction.IwasawaStructure.commutator_lestatement and proof · cited by 4
- Set.powersetCard.fixedPoints_ne_univ_of_faithfulSMulstatement and proof · cited by 3
- CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPointsstatement and proof · cited by 3
- Sylow.fixedPointsMulLeftCosetsEquivQuotientstatement and proof · cited by 2
- FixedPoints.submonoidproof · cited by 2
- IsPGroup.center_nontrivialproof · cited by 2
- CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPointsstatement · cited by 2