theorem Fin2_eq_zero_or_one (k : Fin 2) : k = 0 ∨ k = 1

Every element of Fin 2 is either 0 or 1.

def standardSymplecticAlt (n : ℕ) : Eℝ (2 * n) [⋀^Fin 2]→ₗ[ℝ] ℝ

Standard symplectic alternating $2$-form on $\mathbb{R}^{2n}$: $\Omega(u, v) = \sum_{i=1}^{n} (u_i v_{n+i} - u_{n+i} v_i)$, with the $(e_i, f_i)$ basis given by $f_i = e_{n+i}$ so that $\Omega(e_i, f_j) = \delta_{ij}$.

def standardSymplecticForm (n : ℕ) : EuclideanΩ (2 * n) 2

The standard symplectic $2$-form on $\mathbb{R}^{2n}$ viewed as a constant differential form.

theorem standardSymplecticForm_closed (n : ℕ) : (standardSymplecticForm n).euclideanD_lifted = 0

The standard symplectic form is closed: $d\Omega = 0$ (it is constant in $x$).

theorem standardSymplecticBilinear_nondegenerate (n : ℕ) (u : Eℝ (2 * n)) (h : ∀ (v : Eℝ (2 * n)), ∑ i : Fin n, (u.ofLp ⟨↑i, ⋯⟩ * v.ofLp ⟨n + ↑i, ⋯⟩ - u.ofLp ⟨n + ↑i, ⋯⟩ * v.ofLp ⟨↑i, ⋯⟩) = 0) : u = 0

Bilinear nondegeneracy of the standard symplectic form: if $\Omega(u, v) = 0$ for all $v$, then $u = 0$.

theorem standardSymplecticForm_nondegenerate (n : ℕ) : Function.Injective fun (X : EuclideanVF (2 * n)) => euclideanIota X (standardSymplecticForm n)

Nondegeneracy at the level of vector fields: the contraction $X \mapsto \iota_X \Omega$ is injective on vector fields on $\mathbb{R}^{2n}$.