Theorems · Definition · group theory

Matrix.symplecticGroup

(l : Type u_1) →
  (R : Type u_2) →
    [inst : DecidableEq l] → [inst_1 : CommRing R] → [inst_2 : Fintype l] → Submonoid (Matrix (l ⊕ l) (l ⊕ l) R)

The group of symplectic matrices over a ring R.

Defined in

Mathlib.LinearAlgebra.SymplecticGroup

Cited by

15 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqCommRingFintype