Theorems · Definition · group theory

Matrix.SpecialLinearGroup.lineStab

{F : Type u_1} →
  [inst : Field F] →
    {ι : Type u_2} →
      [inst_1 : DecidableEq ι] → [inst_2 : Fintype ι] → Submodule F (ι → F) → Subgroup (Matrix.SpecialLinearGroup ι F)

The "unipotent radical" attached to a subspace L ⊆ ι → F: the subgroup of SL ι F consisting of matrices A such that A - 1 sends every vector into L. When L is one-dimensional this is an abelian subgroup of the stabilizer of L in SL.

Defined in

Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Cited by

10 results in Mathlib

Foundations

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

Assumes

FieldDecidableEqFintype