Theorems · Theorem · group theory

finite_compl_fixedBy_closure_iff

∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {S : Set G},
  (∀ g ∈ Subgroup.closure S, (MulAction.fixedBy α g)ᶜ.Finite) ↔ ∀ g ∈ S, (MulAction.fixedBy α g)ᶜ.Finite

If the support of each element in a generating set of a permutation group is finite, then the support of every element in the group is finite.

Defined in

Mathlib.GroupTheory.Perm.ClosureSwap

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupMulAction