Theorems · Definition · group theory
Matrix.J
(l : Type u_1) → (R : Type u_2) → [DecidableEq l] → [CommRing R] → Matrix (l ⊕ l) (l ⊕ l) R
The matrix defining the canonical skew-symmetric bilinear form.
- Defined in
- Mathlib.LinearAlgebra.SymplecticGroup
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
- Assumes
- DecidableEqCommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Matrixstatement · cited by 4,303
- Matrix.fromBlocksproof · cited by 108
Cited by23
Results whose statement or proof uses this declaration.
- Matrix.symplecticGroupproof · cited by 15
- SymplecticGroup.mem_iffstatement and proof · cited by 6
- Matrix.J_squaredstatement · cited by 3
- SymplecticGroup.inv_left_mul_auxstatement and proof · cited by 2
- SymplecticGroup.mem_iff'statement and proof · cited by 2
- SymplecticGroup.transpose_memproof · cited by 2
- Matrix.isUnit_det_Jstatement and proof · cited by 1
- SymplecticGroup.coe_invstatement · cited by 1
- SymplecticGroup.map_memproof · cited by 1
- SymplecticGroup.symJproof · cited by 1
- SymplecticGroup.symplectic_detproof · cited by 1
- Matrix.map_Jstatement · cited by 1