Matrix.J_squared

theorem Matrix.J_squared : ∀ (l : Type u_1) (R : Type u_2) [inst : DecidableEq l] [inst_1 : CommRing R] [inst_2 : Fintype l], Matrix.J l R * Matrix.J l R = -1

The theorem `Matrix.J_squared` states that for any type `l`, any type `R` which is a commutative ring, when `l` has decidable equality and is finite, the square of the matrix `J` (which is defined as the canonical skew-symmetric bilinear form) is equal to `-1`. Here, `Matrix.J l R` is a matrix whose elements are of type `R`, and the matrix is defined using the direct sum of type `l`. The multiplication `*` represents the matrix multiplication. The result `-1` is an element of the commutative ring `R`.

More concisely: For any finite, decidably equal commutative ring `R` and finite type `l`, the square of the canonical skew-symmetric matrix `J : Matrix R l` is equal to the negative identity matrix `-1 : Matrix R l`.