Theorems · Theorem · group theory

Function.Injective.mulActionHom_embedding.congr_simp

∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : Group H] [inst_3 : MulAction H β] {σ : G → H} {f f_1 : α →ₑ[σ] β} (e_f : f = f_1) (ι : Type u_5)
  (hf : Function.Injective ⇑f),
  Function.Injective.mulActionHom_embedding ι hf = Function.Injective.mulActionHom_embedding ι ⋯

Defined in

Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupMulActionGroupMulAction