List.ofFn x ~ List.ofFn y

Stream: Is there code for X?

[Martin Dvořák]

Is there an existing definition in Mathlib and API for the following concept?

import Mathlib.Data.List.Perm

def ArePerm {T : Type} {n : ℕ} (x y : Fin n → T) : Prop :=
  List.ofFn x ~ List.ofFn y

[Eric Wieser]

docs#Equiv.Perm.ofFn_comp_perm

[Eric Wieser]

Probably you want an iff version of that

[Yury G. Kudryashov]

I guess (not tested) MulAction.orbitRel (DomMulAct (Equiv.Perm (Fin n)) is what you want.

[Yury G. Kudryashov]

If you're going to add theory about it, then please do it for α → β without finiteness assumptions first.

[Yury G. Kudryashov]

You can define, e.g.,

def DomConj (f : α → γ) (g : β → γ) : Prop := ∃ e : α ≃ β, f = g ∘ e