disjoint

Stream: mathlib4

[vxctyxeha]

How to indicate that two permutations are disjoint

[Aaron Liu]

Can you give a definition of what it means for two permutations to be disjoint?

[vxctyxeha]

disjoint

[Damiano Testa]

More effort when posing a question is definitely important to entice people to answer your questions.

[vxctyxeha]

well the question is Compute explicitly three conjugates of the permutation

(145)(96)(237),checking that its disjoint cycle structure is preserved

[vxctyxeha]

my point is how to represent disjoint,and is the code below equivalent to qusetion,what is the difference between cycle type and disjoint

import Mathlib

theorem isConj_iff_cycleType_eq_theorem_internal_vars :
  ∀ {α : Type*} [Fintype α] [DecidableEq α] (σ τ : Equiv.Perm α),
    IsConj σ τ ↔ σ.cycleType = τ.cycleType :=by
    exact fun {α} [Fintype α] [DecidableEq α] σ τ => Equiv.Perm.isConj_iff_cycleType_eq

[vxctyxeha]

Or more simply is permutation a set

[Aaron Liu]

Are you looking for docs#Equiv.Perm.Disjoint