Theorems · Definition · group theory

SpecialLinearGroup

(R : Type u_1) → (V : Type u_2) → [inst : CommRing R] → [inst_1 : AddCommGroup V] → [Module R V] → Type (max 0 u_2)

The special linear group of a module. This is only meaningful when the module is finite and free, for otherwise, it coincides with the group of linear equivalences.

Defined in

Mathlib.LinearAlgebra.SpecialLinearGroup

Cited by

43 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule