Theorems · Definition · group theory
AddAction.fixedBy
{M : Type u_1} → (α : Type u_3) → [inst : AddMonoid M] → [AddAction M α] → M → Set αfixedBy m is the set of elements fixed by m.
- Defined in
- Mathlib.GroupTheory.GroupAction.Defs
- Cited by
- 26 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.
Cites5
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
- AddMonoidstatement and proof · cited by 2,864
- HVAdd.hVAddproof · cited by 1,820
- AddActionstatement and proof · cited by 820
Cited by27
Results whose statement or proof uses this declaration.
- AddAction.mem_fixedBystatement · cited by 12
- AddAction.fixedBy_negstatement and proof · cited by 3
- AddAction.mem_fixedBy_zsmulstatement and proof · cited by 2
- AddAction.movedBy_mem_fixedBy_of_addCommutestatement and proof · cited by 2
- AddAction.vadd_mem_fixedBy_iff_mem_fixedBystatement and proof · cited by 2
- AddAction.fixedBy_mem_fixedBy_of_addCommutestatement and proof · cited by 2
- AddAction.fixedBy_subset_fixedBy_zsmulstatement and proof · cited by 2
- AddAction.set_mem_fixedBy_iffstatement · cited by 1
- AddAction.set_mem_fixedBy_of_movedBy_subsetstatement and proof · cited by 1
- AddAction.sigmaFixedByEquivOrbitsProdAddGroupstatement and proof · cited by 1
- mem_fixingAddSubgroup_compl_iff_movedBy_subsetstatement and proof · cited by 1
- mem_fixingAddSubgroup_iff_subset_fixedBystatement and proof · cited by 1