Theorems · Theorem · group theory

Equiv.Perm.isConj_of_support_equiv

∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {σ τ : Equiv.Perm α}
  (f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }),
  (∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)) → IsConj σ τ

Defined in

Mathlib.GroupTheory.Perm.Finite

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype