Theorems · Definition · group theory

Matrix.SpecialLinearGroup

(n : Type u) → [DecidableEq n] → [Fintype n] → (R : Type v) → [CommRing R] → Type (max 0 u v)

SpecialLinearGroup n R is the group of n by n R-matrices with determinant equal to 1.

Defined in

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Cited by

348 results in Mathlib

Foundations

Depth 87 from the axioms, rests on 2,566 definitions · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeCommRing