mapGL_coe_matrix

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

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

English

The determinant of the image of a special linear matrix under mapGL is 1.

Русский

Определитель изображения матрицы Special Linear через mapGL равен 1.

LaTeX

$$((\\mathrm{mapGL}\\,S\\ g).\\det) = 1$$

Lean4

@[simp]
theorem mapGL_coe_matrix (g : SpecialLinearGroup n R) : ((mapGL S g) : Matrix n n S) = g.map (algebraMap R S) :=
  rfl

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

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

Разделы

Аффилиация

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