Mathlib Map

Theorems · Theorem · group theory

mem_fixingSubgroup_iff

∀ (M : Type u_1) {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} {m : M},
  m ∈ fixingSubgroup M s ↔ ∀ y ∈ s, m • y = y
Defined in
Mathlib.GroupTheory.GroupAction.FixingSubgroup
Cited by
8 results in Mathlib
Foundations
Depth 17 from the axioms · uses propext
Assumes
GroupMulAction
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SubMulAction.IsPretransitive.isPretransitive_ofFixingSubgroup_inter · cited by 2IsPretransitive.isPretran…MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl · cited by 2IsBlock.compl_subset_of_s…Equiv.Perm.isPretransitive_of_isCycle_mem · cited by 2Perm.isPretransitive_of_i…SubMulAction.ofFixingSubgroup_of_singleton · cited by 1SubMulAction.ofFixingSubg…SubMulAction.ofFixingSubgroup_of_singleton_bijective · cited by 1SubMulAction.ofFixingSubg…IntermediateField.mem_fixingSubgroup_iff · cited by 1IntermediateField.mem_fix…MulAction.IsMultiplyPreprimitive.of_bijective_map · cited by 1IsMultiplyPreprimitive.of…InfiniteGalois.fixingSubgroup_fixedField · cited by 0InfiniteGalois.fixingSubg…InfiniteGalois.fixingSubgroup_isClosed · cited by 0InfiniteGalois.fixingSubg…Set · cited by 53352SetSet.Elem · cited by 7166Set.ElemGroup · cited by 6238GroupSubgroup · cited by 3593SubgroupMulAction · cited by 1294MulActionfixingSubgroup · cited by 83fixingSubgroupmem_fixingSubgroup_iffCITED BYCITES

Cites6

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
  • MulActionstatement and proof · cited by 1,294
  • fixingSubgroupstatement and proof · cited by 83

Cited by9

Results whose statement or proof uses this declaration.