Theorems · Theorem · group theory

AddAction.IsPretransitive.of_embedding_congr

∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : AddGroup H] [inst_3 : AddAction H β] {σ : G → H} {f : α →ₑ[σ] β} {n : Type u_5},
  Function.Surjective σ →
    Function.Bijective ⇑f → (AddAction.IsPretransitive G (n ↪ α) ↔ AddAction.IsPretransitive H (n ↪ β))

Defined in

Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddGroupAddActionAddGroupAddAction