Theorems · Theorem · group theory

MulAction.IsBlock.image

∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X} {H : Type u_3} {Y : Type u_4}
  [inst_2 : SMul H Y] {φ : G → H} (j : X →ₑ[φ] Y),
  Function.Surjective φ → Function.Injective ⇑j → MulAction.IsBlock G B → MulAction.IsBlock H (⇑j '' B)

Defined in

Mathlib.GroupTheory.GroupAction.Blocks

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupMulActionSMul