coeToGL_det

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

URI: https://scilib.ai/kg/mathlib#Matrix.SpecialLinearGroup.coeToGL_det

English

The underlying matrix of toGL(g) equals g itself.

Русский

Матрица, лежащая в основе toGL(g), равна g.

LaTeX

$$((\\mathrm{toGL} g):\\,\\mathrm{Matrix}_{n\\times n} R) = g$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru