Keyword: group-scheme

Definition Chevalley Group Construction from a Root Datum admitted

Definition General Linear Group Scheme GL(V) formalized

Definition Homomorphism of Affine Group Schemes admitted

Definition Special Linear Group Scheme SL_n admitted

Definition Special Orthogonal Group Scheme SO_n admitted

Definition Symplectic Group Scheme Sp_{2n} admitted

Definition The Diagonalizable Group Scheme D(M) admitted