Theorems · Definition · group theory
MulAction.fixedBy
{M : Type u_1} → (α : Type u_3) → [inst : Monoid M] → [MulAction M α] → M → Set αfixedBy m is the set of elements fixed by m.
- Defined in
- Mathlib.GroupTheory.GroupAction.Defs
- Cited by
- 36 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 by38
Results whose statement or proof uses this declaration.
- MulAction.mem_fixedBystatement · cited by 6
- MulAction.fixedBy_invstatement and proof · cited by 4
- mem_closure_isSwapstatement and proof · cited by 2
- MulAction.smul_mem_fixedBy_iff_mem_fixedBystatement and proof · cited by 2
- MulAction.mem_fixedBy_zpowstatement and proof · cited by 2
- card_comm_eq_card_conjClasses_mul_cardproof · cited by 2
- MulAction.movedBy_mem_fixedBy_of_commutestatement and proof · cited by 2
- MulAction.fixedBy_eq_univ_iff_eq_onestatement and proof · cited by 2
- MulAction.fixedBy_mem_fixedBy_of_commutestatement and proof · cited by 2
- MulAction.fixedBy_subset_fixedBy_zpowstatement and proof · cited by 2
- MulAction.set_mem_fixedBy_iffstatement · cited by 1
- MulAction.set_mem_fixedBy_of_movedBy_subsetstatement and proof · cited by 1