coe_to_GLPos_to_GL_det — Mathlib

English

For any g in SpecialLinearGroup, the determinant of its image in GL from GLPos is 1, since all elements in SL have determinant 1.

Русский

Для любого g в SL(n,R) детерминант образа g в GL через GLPos равен 1, поскольку элементы SL имеют det = 1.

LaTeX

$$$\det\bigl((g : GL^+(n,R)) : GL(n,R)\bigr) = 1.$$$

Lean4

@[simp]
theorem coe_to_GLPos_to_GL_det (g : SpecialLinearGroup n R) :
    Matrix.GeneralLinearGroup.det ((g : GLPos n R) : GL n R) = 1 :=
  Units.ext g.prop

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