theorem SymplecticLinearAlgebra.symplectic_even_dim {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {Ω : LinearMap.BilinForm ℝ V} (hΩ : IsSymplecticForm Ω) : Even (Module.finrank ℝ V)

A real vector space carrying a symplectic form must have even dimension: if $\Omega$ is a nondegenerate alternating form on $V$, then $\dim_\mathbb{R} V \in 2\mathbb{N}$.