Documentation

Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup

Projective Special Linear Group #

Notation #

In the MatrixGroups locale:

@[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.

Equations
Instances For

    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.
    Instances For