Theorems · Theorem · group theory

MulAction.set_mem_fixedBy_iff

∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (s : Set α) (g : G),
  s ∈ MulAction.fixedBy (Set α) g ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s

If a set s : Set α is in fixedBy (Set α) g, then all points of s will stay in s after being moved by g.

Defined in

Mathlib.GroupTheory.GroupAction.FixedPoints

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound

Assumes

GroupMulAction