Theorems · Theorem · group theory

Set.powersetCard.isPretransitive_alternatingGroup

∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
  3 ≤ Nat.card α → MulAction.IsPretransitive ↥(alternatingGroup α) ↑(Set.powersetCard α n)

If 3 ≤ Nat.card α, then alternatingGroup α acts transitively on Set.powersetCard α n. If Nat.card α ≤ 2, then alternatingGroup α is trivial, and the result only holds in the trivial case where powersetCard α n is a subsingleton, that is, when n = 0 or Nat.card α ≤ n.

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype