Theorems · Definition · group theory

Matrix.ProjGenLinGroup

(n : Type u_1) → [Fintype n] → [DecidableEq n] → (R : Type u_2) → [CommRing R] → Type (max (max u_1 u_2) u_2 u_1)

Projective general linear group $PGL(n, R)$ defined as the quotient of the general linear group by its center.

Defined in

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Cited by

23 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqCommRing