Projective Special Linear Group

Notation

In the MatrixGroups locale:

• PSL(n, R) is a shorthand for Matrix.ProjectiveSpecialLinearGroup (Fin n) R

@[reducible, inline]

abbrev Matrix.ProjectiveSpecialLinearGroup (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] : Type (max (max u v) v u)

A projective special linear group is the quotient of a special linear group by its center.

def MatrixGroups.«termPSL(_,_)» : Lean.ParserDescr

PSL(n, R) is the projective special linear group SL(n, R)/Z(SL(n, R)).