det_coe

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

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

English

For every matrix A in SL(n, R), the determinant is 1.

Русский

Для каждой матрицы A из SL(n, R) детерминант равен 1.

LaTeX

$$$A \in \mathrm{SL}_n(R) \Rightarrow \det(A) = 1$$$

Lean4

@[simp]
theorem det_coe : det ↑ₘA = 1 :=
  A.2

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

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

Разделы

Аффилиация

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