Theorems · Theorem · group theory
MulAction.IsMultiplyPreprimitive.isMultiplyPretransitive
∀ (M : Type u_1) (α : Type u_2) {inst : Group M} {inst_1 : MulAction M α} (n : ℕ)
[self : MulAction.IsMultiplyPreprimitive M α n], MulAction.IsMultiplyPretransitive M α nAn n-preprimitive action is n-pretransitive.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- MulActionstatement and proof · cited by 1,294
- MulAction.IsMultiplyPretransitivestatement · cited by 33
- MulAction.IsMultiplyPreprimitivestatement and proof · cited by 17
Cited by5
Results whose statement or proof uses this declaration.
- Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_memproof · cited by 2
- MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizerproof · cited by 2
- Equiv.Perm.subgroup_eq_top_of_isPreprimitive_of_isSwap_memproof · cited by 1
- MulAction.isMultiplyPreprimitive_ofStabilizerproof · cited by 1
- MulAction.isMultiplyPreprimitive_congrproof · cited by 0