Theorems · Theorem · group theory

MulAction.IsPreprimitive.of_surjective

∀ {M : Type u_3} [inst : Group M] {α : Type u_4} [inst_1 : MulAction M α] {N : Type u_5} {β : Type u_6}
  [inst_2 : Group N] [inst_3 : MulAction N β] {φ : M → N} {f : α →ₑ[φ] β} [MulAction.IsPreprimitive M α],
  Function.Surjective ⇑f → MulAction.IsPreprimitive N β

Defined in

Mathlib.GroupTheory.GroupAction.Primitive

Cited by

8 results in Mathlib

Foundations

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

Assumes

GroupMulActionGroupMulActionMulAction.IsPreprimitive