Theorems · Theorem · group theory
Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem
∀ {α : Type u_1} {G : Subgroup (Equiv.Perm α)} [inst : Fintype α] [inst_1 : DecidableEq α],
MulAction.IsPreprimitive (↥G) α → ∀ {g : Equiv.Perm α}, g.IsThreeCycle → g ∈ G → alternatingGroup α ≤ GA primitive subgroup of Equiv.Perm α that contains a 3-cycle
contains the alternating group (Jordan).
- Defined in
- Mathlib.GroupTheory.GroupAction.Jordan
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FintypeDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites50
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setproof · cited by 53,352
- SetLike.coeproof · cited by 8,199
- Fintypestatement and proof · cited by 7,736
- mul_oneproof · cited by 3,885
- Subgroupstatement and proof · cited by 3,593
- Finset.univproof · cited by 3,473
- Compl.complproof · cited by 2,925
- zero_addproof · cited by 2,366
- Finset.cardproof · cited by 2,327
- Nat.Primeproof · cited by 2,059
- add_commproof · cited by 1,535
Cited by2
Results whose statement or proof uses this declaration.
- alternatingGroup.subgroup_eq_top_of_isPreprimitiveproof · cited by 1
- Equiv.Perm.alternatingGroup_le_of_isPreprimitiveproof · cited by 0