ProjectiveSpecialLinearGroup — Mathlib

English

The projective special linear group PSL(n, R) is the quotient of the special linear group SL(n, R) by its center Z(SL(n, R)).

Русский

Проективная специальная линейная группа PSL(n, R) является фактор-группой SL(n, R) по центру Z(SL(n, R)).

LaTeX

$$$\mathrm{PSL}_n(R) = \mathrm{SL}_n(R) / Z(\mathrm{SL}_n(R)).$$$

Lean4

/-- A projective special linear group is the quotient of a special linear group by its center. -/
abbrev ProjectiveSpecialLinearGroup : Type _ :=
  SpecialLinearGroup n R ⧸ Subgroup.center (SpecialLinearGroup n R)

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