English
signAux2 is defined recursively on a list l of elements: signAux2([], f) = 1; signAux2(x :: l, f) = if x = f x then signAux2(l, f) else - signAux2(l, swap x (f x) · f).
Русский
signAux2 определено по рекурсии на списке l элементов: signAux2([], f) = 1; signAux2(x :: l, f) = если x = f x, то signAux2(l, f), иначе - signAux2(l, swap x (f x) · f).
LaTeX
$$$\text{signAux2}([], f) = 1,\; \text{signAux2}(x::l, f) = \begin{cases} \text{signAux2}(l,f), & x = f(x) \\ -\text{signAux2}(l,\; \text{swap } x (f x) \cdot f), & \text{однако } x \neq f(x) \end{cases}$$$
Lean4
/-- When the list `l : List α` contains all nonfixed points of the permutation `f : Perm α`,
`signAux2 l f` recursively calculates the sign of `f`. -/
def signAux2 : List α → Perm α → ℤˣ
| [], _ => 1
| x :: l, f => if x = f x then signAux2 l f else -signAux2 l (swap x (f x) * f)
