Theorems · Theorem · group theory

AddAction.isMultiplyPreprimitive_congr

∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {N : Type u_3} {β : Type u_4}
  [inst_2 : AddGroup N] [inst_3 : AddAction N β] {φ : M → N},
  Function.Surjective φ →
    ∀ {f : α →ₑ[φ] β},
      Function.Bijective ⇑f → ∀ {n : ℕ}, AddAction.IsMultiplyPreprimitive M α n ↔ AddAction.IsMultiplyPreprimitive N β n

Defined in

Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupAddActionAddGroupAddAction