skew_symmetric_rank_conjecture
Provedcombinatoricsgraph-theorynumber-theory
Skew-symmetric matrix rank parity: Any skew-symmetric matrix over ℝ has even rank. Proved since eigenvalues come in ±iλ pairs. Applications to combinatorics: a tournament has an odd number of Hamiltonian cycles iff its skew-adjacency matrix has full rank.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem skew_symmetric_rank_conjecture (n : ℕ) (hn : 2 ≤ n)
(A : Matrix (Fin n) (Fin n) ℝ)
(hskew : A = -A.transpose)
(hrank : A.rank ≥ n - 1) :
A.rank = n - 1 ∨ A.rank = n := by
sorrySource