Theorems · Definition · group theory

alternatingGroup.iwasawaStructure_four

{α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] → 5 ≤ Nat.card α → MulAction.IwasawaStructure ↥(alternatingGroup α) ↑(Set.powersetCard α 4)

The Iwasawa structure of alternatingGroup α acting on Set.powersetCard α 4, provided α has at least 5 elements.

Defined in: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Cited by: 1 results in Mathlib
Foundations: Depth 130 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Finsetstatement · cited by 13,712
Fintypestatement and proof · cited by 7,736
Set.Elemstatement and proof · cited by 7,166
Subgroupstatement · cited by 3,593
Equiv.Permstatement · cited by 1,375
Nat.cardstatement and proof · cited by 844
Subgroup.mapproof · cited by 301
Set.powersetCardstatement and proof · cited by 100
alternatingGroupstatement · cited by 96
alternatingGroup.kleinFourproof · cited by 11
alternatingGroup.ofSubtypeproof · cited by 9
MulAction.IwasawaStructurestatement · cited by 8

Cited by1

Results whose statement or proof uses this declaration.

alternatingGroup.normal_subgroup_eq_bot_or_eq_top_of_card_ne_eightproof · cited by 1