Theorems · Theorem · group theory

Group.preimage_smul_set

∀ {G : Type u_1} [inst : Group G] {α : Type u_2} {β : Type u_3} [inst_1 : MulAction G α] [inst_2 : MulAction G β]
  {F : Type u_4} [inst_3 : FunLike F α β] [MulActionHomClass F G α β] (f : F) (c : G) (t : Set β),
  ⇑f ⁻¹' (c • t) = c • ⇑f ⁻¹' t

Defined in

Mathlib.GroupTheory.GroupAction.Pointwise

Cited by

0 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Quot.sound

Assumes

GroupMulActionMulActionFunLikeMulActionHomClass