Theorems · Theorem · group theory
MulAction.isPreprimitive_of_is_two_pretransitive
∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
MulAction.IsMultiplyPretransitive G α 2 → MulAction.IsPreprimitive G αA 2-transitive action is primitive.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Top.topproof · cited by 9,680
- Groupstatement and proof · cited by 6,238
- MulActionstatement and proof · cited by 1,294
- Set.Subsingletonproof · cited by 276
- eq_top_iffproof · cited by 236
- Set.Nontrivialproof · cited by 145
- MulAction.IsPretransitiveproof · cited by 94
- MulAction.IsBlockproof · cited by 73
- MulAction.IsPreprimitivestatement · cited by 50
- Set.smul_mem_smul_setproof · cited by 39
- MulAction.IsMultiplyPretransitivestatement and proof · cited by 33
Cited by3
Results whose statement or proof uses this declaration.
- alternatingGroup.isTrivialBlock_of_isBlockproof · cited by 1
- MulAction.isMultiplyPreprimitive_of_isMultiplyPretransitive_succproof · cited by 1
- normalClosure_of_stabilizer_eq_topproof · cited by 0