This problem arose from studying the book Lectures on the Geometry of Manifolds: Suppose $V$ is a real vector space, and $\omega : V \times V \to \mathbb{R}$ is a symplectic duality, then $V$ has even dimension.

I can make some concrete computation on dimension 2 and 3 and roughly understand the reason, but I have no general proof.

After a month, I found a solution:

Proof. Using the properties of matrix column operations [math-000W]

2025-05-12

Since the multiplication factor of a matrix column can be extracted as a basis, flip the column 1 (i.e. the whole column multiply $-1$ ) we have

\det(A) = -1 \cdot \det(A_{\text{flip1}})

Following this pattern, flipping column 2 gives us:

\det(A) = (-1) \cdot (-1) \cdot \det(A_{\text{flip1,flip2}})

Let $A$ be an $n \times n$ skew-symmetric matrix. After flipping all $n$ columns, we obtain $-A$ , therefore

\det(A) = (-1)^n \cdot \det(-A)

By definition, skew-symmetric means $-A = A^T$ , so

\det(A) = (-1)^n \cdot \det(A^T)

When $n$ is odd, this gives us

\det(A) = -\det(A^T) = -\det(A)

Therefore $\det(A)$ must be 0.

After formalize this statement https://github.com/dannypsnl/blackboard/commit/2c0de90a98c24ae57bd30bc47ed8c3b6a75f2664, I found this need the field is charateristic 0, sure $\mathbb{R}$ indeed satisfies that, this point to me is that Lean can help me refine my ideas.

If $A$ represents a duality, then $\det(A) \neq 0$ . Therefore $n$ cannot be odd—it must be even.