Special linear groups

Stream: Is there code for X?

[Antoine Chambert-Loir]

Mathlib has a docs#Matrix.SpecialLinearGroup for the group of matrices of determinant 1. But is there already the analogue special linear group acting on any finite dimensional module of finite rank?
(Or course, one can define it as the kernel of the determinant group morphism.)