Theorems · Theorem · group theory

AddAction.isPreprimitive_of_is_two_pretransitive

∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α],
  AddAction.IsMultiplyPretransitive G α 2 → AddAction.IsPreprimitive G α

A 2-transitive additive action is primitive.

Defined in: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Cited by: 1 results in Mathlib
Foundations: Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddGroup AddAction

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites18

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
AddGroupstatement and proof · cited by 4,410
HVAdd.hVAddproof · cited by 1,820
AddActionstatement and proof · cited by 820
Set.Subsingletonproof · cited by 276
eq_top_iffproof · cited by 236
Set.Nontrivialproof · cited by 145
AddAction.IsBlockproof · cited by 65
AddAction.IsPretransitiveproof · cited by 56
AddAction.IsPreprimitivestatement · cited by 25
AddAction.IsMultiplyPretransitivestatement and proof · cited by 17

Cited by1

Results whose statement or proof uses this declaration.

AddAction.isMultiplyPreprimitive_of_isMultiplyPretransitive_succproof · cited by 1