Projective Special Linear Group

Notation

In the MatrixGroups locale:

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

@[inline, reducible]

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.

Equations

• Matrix.ProjectiveSpecialLinearGroup n R = (Matrix.SpecialLinearGroup n R ⧸ Subgroup.center (Matrix.SpecialLinearGroup n R))

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

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

Equations

• One or more equations did not get rendered due to their size.