SpecialLinearGroup — Mathlib

English

The special linear group SL(n,R) consists of all n×n matrices over R with determinant equal to 1.

Русский

Специальная линейная группа SL(n,R) состоит из всех матриц n×n над кольцом R детерминант которых равен 1.

LaTeX

$$$\mathrm{SL}_n(R) = \{ A \in \mathrm{M}_n(R) : \det A = 1 \}$$$

Lean4

/-- `SpecialLinearGroup n R` is the group of `n` by `n` `R`-matrices with determinant equal to 1.
-/
def SpecialLinearGroup :=
  { A : Matrix n n R // A.det = 1 }

Похожие утверждения