Mathlib Map

Theorems · Definition · group theory

fixingSubmonoid

(M : Type u_1) → {α : Type u_2} → [inst : Monoid M] → [MulAction M α] → Set α → Submonoid M

The submonoid fixing a set under a MulAction.

Defined in
Mathlib.GroupTheory.GroupAction.FixingSubgroup
Cited by
5 results in Mathlib
Foundations
Depth 9 from the axioms · uses no axioms
Assumes
MonoidMulAction
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

fixingSubgroup · cited by 83fixingSubgroupfixingSubmonoid_fixedPoints_gc · cited by 6fixingSubmonoid_fixedPoin…fixingSubmonoid_union · cited by 0fixingSubmonoid_unionfixingSubmonoid_antitone · cited by 0fixingSubmonoid_antitonefixingSubmonoid_iUnion · cited by 0fixingSubmonoid_iUnionmem_fixingSubmonoid_iff · cited by 0mem_fixingSubmonoid_iffSet · cited by 53352SetSet.Elem · cited by 7166Set.ElemSet.ofPred · cited by 6101Set.ofPredMonoid · cited by 3887MonoidSubmonoid · cited by 3086SubmonoidMulAction · cited by 1294MulActionfixingSubmonoidCITED 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
  • Set.ofPredproof · cited by 6,101
  • Monoidstatement and proof · cited by 3,887
  • Submonoidstatement · cited by 3,086
  • MulActionstatement and proof · cited by 1,294

Cited by6

Results whose statement or proof uses this declaration.