def
Matrix.SpecialLinearGroup.diagonalSubgroup
(n : Type u_1)
[DecidableEq n]
[Fintype n]
(R : Type u_2)
[CommRing R]
:
Subgroup (SpecialLinearGroup n R)
The group of invertible diagonal matrices with determinant 1.
The group of invertible diagonal matrices with determinant 1.