Theorems · Theorem · group theory

fixingAddSubmonoid_fixedPoints_gc

∀ (M : Type u_1) (α : Type u_2) [inst : AddMonoid M] [inst_1 : AddAction M α],
  GaloisConnection (⇑OrderDual.toDual ∘ fixingAddSubmonoid M)
    ((fun P => AddAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)

Defined in

Mathlib.GroupTheory.GroupAction.FixingSubgroup

Cited by

6 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoidAddAction