« Home

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

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-1 ) we have

det⁡(A)=−1⋅det⁡(Aflip1)\det(A) = -1 \cdot \det(A_{\text{flip1}})

Following this pattern, flipping column 2 gives us:

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

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

det⁡(A)=(−1)n⋅det⁡(−A)\det(A) = (-1)^n \cdot \det(-A)

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

det⁡(A)=(−1)n⋅det⁡(AT)\det(A) = (-1)^n \cdot \det(A^T)

When nn is odd, this gives us

det⁡(A)=−det⁡(AT)=−det⁡(A)\det(A) = -\det(A^T) = -\det(A)

Therefore det⁡(A)\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 R\mathbb{R} indeed satisfies that, this point to me is that Lean can help me refine my ideas.

If AA represents a duality, then det⁡(A)≠0\det(A) \neq 0 . Therefore nn cannot be odd—it must be even.