Theorems · Theorem · group theory

AddAction.IsQuasiPreprimitive.isPretransitive_of_normal

∀ {G : Type u_1} {X : Type u_2} {inst : AddGroup G} {inst_1 : AddAction G X} [self : AddAction.IsQuasiPreprimitive G X]
  {N : AddSubgroup G} [N.Normal], AddAction.fixedPoints (↥N) X ≠ Set.univ → AddAction.IsPretransitive (↥N) X

Defined in: Mathlib.GroupTheory.GroupAction.Primitive
Cited by: 0 results in Mathlib
Foundations: Depth 22 from the axioms · uses propext
Assumes: AddAction.IsQuasiPreprimitive AddSubgroup.Normal

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

Setstatement · cited by 53,352
AddGroupstatement and proof · cited by 4,410
Set.univstatement · cited by 3,945
AddSubgroupstatement · cited by 3,232
AddActionstatement and proof · cited by 820
AddSubgroup.Normalstatement · cited by 183
AddAction.IsPretransitivestatement · cited by 56
AddAction.fixedPointsstatement · cited by 20
AddAction.IsQuasiPreprimitivestatement and proof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.