inverse number

Stream: mathlib4

[BANGJI HU]

For a permutation, is there a way to calculate its inverse ordinal number in mathlib?

[BANGJI HU]

import Mathlib
namespace UnexploredExercise_5256_1

def toFun₀ : Fin 5 → Fin 5
  | 1 => 2
  | 2 => 4
  | 3 => 5
  | 4 => 1
  | 5 => 3

def invFun₀ : Fin 5 → Fin 5
  | 1 => 4
  | 2 => 1
  | 3 => 5
  | 4 => 2
  | 5 => 3
def a : Equiv.Perm (Fin 5) := {
  toFun := toFun₀ -- Set the forward function of the permutation to `toFun₀`.
  invFun := invFun₀ -- Set the inverse function of the permutation to `invFun₀`.
  left_inv x := by -- Prove that `invFun₀` is the left inverse of `toFun₀`, i.e., $\text{invFun₀}(\text{toFun₀}(x)) = x$ for all $x \in \text{Fin } 7$.
    fin_cases x <;> decide -- Perform case analysis on all possible values of $x \in \text{Fin } 7$. `decide` tactic is used to automatically verify the equality in each case by computation.
  right_inv x := by -- Prove that `invFun₀` is the right inverse of `toFun₀`, i.e., $\text{toFun₀}(\text{invFun₀}(x)) = x$ for all $x \in \text{Fin } 7$.
    fin_cases x <;> decide -- Perform case analysis on all possible values of $x \in \text{Fin } 7$. `decide` tactic is used to automatically verify the equality in each case by computation.
}
def myInvCount {n : ℕ} (σ : Equiv.Perm (Fin n)) : ℕ :=
  let all_pairs := Finset.product (Finset.univ : Finset (Fin n)) (Finset.univ : Finset (Fin n))
  let inversion_pairs := all_pairs.filter (fun (i, j) => i < j ∧ σ j < σ i)
  inversion_pairs.card
theorem manual_invCount_of_a_is_5 : myInvCount a = 5 := by

[Aaron Liu]

Are you looking for docs#Equiv.Perm.sign

[Aaron Liu]

Hmm, it looks like you want the Finset.card of docs#Equiv.Perm.finPairsLT

[Aaron Liu]

I don't think what you want is in mathlib