Talk:Permutation of Determinant Indices

Little detail in the proof

The proof contains a definition of $\nu$ such that $\lambda \circ \nu = \mu$. Actually, I think it must be $\nu \circ \lambda = \mu$. --Roglo (talk) 00:32, 15 June 2021 (UTC)

Possibly. Can't get my head round it this morning. Can you explain your thinking? --prime mover (talk) 06:02, 15 June 2021 (UTC)

Because, just below "The product can be rearranged as", the expression $a_{\map \lambda 1, \map \mu 1} a_{\map \lambda 2, \map \mu 2} \cdots a_{\map \lambda n, \map \mu n}$ is not equal to $a_{1, \map \nu 1} a_{2, \map \nu 2} \cdots a_{n, \map \nu n}$ as printed.

Indeed, for some $i$, there is a factor $a_{\map \lambda i, \map \mu i}$ where $\map \lambda i = 1$, but, in that case, $\map \mu i$ is not equal to $\map \nu 1$ but to $\map {\lambda \circ \nu} i = \map \lambda {\map \nu i}$ which is not $\map \nu 1$. On the other hand, with $\nu \circ \lambda = \mu$, as I claim, we get $\map \mu i = \map {\nu \circ \lambda} i = \map \nu {\map \lambda i} = \map \nu 1$. I found that while translating this proof into the Coq proof assistant, which checks everything we write. --Roglo (talk) 07:52, 15 June 2021 (UTC)

I'm not in a position to get my head round it at the moment, so if you want to make whatever adjustments are necessary, please feel free. --prime mover (talk) 20:14, 15 June 2021 (UTC)

Okay, no problem. --Roglo (talk) 22:35, 15 June 2021 (UTC)