hasOne

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

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

English

The identity element is the 2×2 identity matrix (det = 1) and lies in SL(n,R).

Русский

Единичный элемент — это единичная матрица размерности n×n и принадлежит SL(n,R).

LaTeX

$$One (SpecialLinearGroup n R)$$

Lean4

instance hasOne : One (SpecialLinearGroup n R) :=
  ⟨⟨1, det_one⟩⟩

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

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

Разделы

Аффилиация

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