[proofplan] We write out the Leibniz formula for $\det A^\top$, substitute $(A^\top)_{i,\sigma(i)} = A_{\sigma(i),i}$, and reindex the sum via the substitution $\tau = \sigma^{-1}$. Since inversion is a bijection on $S_n$ and $\varepsilon(\sigma^{-1}) = \varepsilon(\sigma)$, the reindexed sum equals $\det A$. [/proofplan] [step:Write the Leibniz formula for $\det A^\top$] By the Leibniz formula and the definition $(A^\top)_{ij} = A_{ji}$: \begin{align*} \det A^\top = \sum_{\sigma \in S_n} \varepsilon(\sigma) \prod_{i=1}^n (A^\top)_{i,\sigma(i)} = \sum_{\sigma \in S_n} \varepsilon(\sigma) \prod_{i=1}^n A_{\sigma(i),i}. \end{align*} [/step] [step:Reindex via $\tau = \sigma^{-1}$ to recover $\det A$] We substitute $\tau = \sigma^{-1}$. Since $\sigma \mapsto \sigma^{-1}$ is a bijection on $S_n$ and $\varepsilon(\sigma^{-1}) = \varepsilon(\sigma)$, the sum can be rewritten over $\tau$. As $i$ ranges over $\{1, \dots, n\}$, the pair $(\sigma(i), i)$ ranges over $\{(\sigma(1), 1), \dots, (\sigma(n), n)\}$. Setting $j = \sigma(i)$ (equivalently $i = \tau(j)$), the product becomes \begin{align*} \prod_{i=1}^n A_{\sigma(i),i} = \prod_{j=1}^n A_{j, \tau(j)}. \end{align*} Therefore: \begin{align*} \det A^\top = \sum_{\tau \in S_n} \varepsilon(\tau) \prod_{j=1}^n A_{j, \tau(j)} = \det A. \end{align*} [guided] The Leibniz formula for $\det A$ sums over permutations with the product $\prod_{i=1}^n A_{i,\sigma(i)}$ -- the entries are picked by choosing one from each row, with the column determined by $\sigma$. For $\det A^\top$, we get $\prod_{i=1}^n A_{\sigma(i),i}$ -- now the row is determined by $\sigma$ and the column is fixed at $i$. These two expressions look different, but they produce the same set of products. The substitution $\tau = \sigma^{-1}$ makes this precise. If $\sigma(i) = j$, then $\tau(j) = i$, so the factor $A_{\sigma(i),i} = A_{j,\tau(j)}$. As $i$ ranges over $\{1, \dots, n\}$, the index $j = \sigma(i)$ also ranges over $\{1, \dots, n\}$ (since $\sigma$ is a bijection). So \begin{align*} \prod_{i=1}^n A_{\sigma(i),i} = \prod_{j=1}^n A_{j,\tau(j)}. \end{align*} Since $\varepsilon(\tau) = \varepsilon(\sigma^{-1}) = \varepsilon(\sigma)$ and $\sigma \mapsto \tau$ is a bijection on $S_n$: \begin{align*} \det A^\top = \sum_{\sigma \in S_n} \varepsilon(\sigma) \prod_{i=1}^n A_{\sigma(i),i} = \sum_{\tau \in S_n} \varepsilon(\tau) \prod_{j=1}^n A_{j,\tau(j)} = \det A. \end{align*} The geometric content: the determinant does not distinguish between rows and columns. Any property of column operations has a dual statement about row operations, and vice versa. [/guided] [/step]