Theorems · Theorem · group theory

AddAction.IsPreprimitive.of_card_lt

∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] {H : Type u_3} {Y : Type u_4}
  [inst_2 : AddGroup H] [inst_3 : AddAction H Y] {φ : G → H} {f : X →ₑ[φ] Y} [Finite Y] [AddAction.IsPretransitive H Y]
  [AddAction.IsPreprimitive G X], Nat.card Y < 2 * (Set.range ⇑f).ncard → AddAction.IsPreprimitive H Y

The codomain of an equivariant map of large image is preprimitive if the domain is.

Defined in

Mathlib.GroupTheory.GroupAction.Primitive

Cited by

0 results in Mathlib

Foundations

Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddActionAddGroupAddActionFiniteAddAction.IsPretransitiveAddAction.IsPreprimitive