transpose

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

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

← MathLib Explorer

English

The transpose of a matrix in SL(n,R) is again in SL(n,R).

Русский

Транспонирование матрицы из SL(n,R) даёт матрицу снова из SL(n,R).

LaTeX

$$transpose (A) ∈ \mathrm{SL}_n(R) for A ∈ \mathrm{SL}_n(R)$$

Lean4

/-- The transpose of a matrix in `SL(n, R)` -/
def transpose (A : SpecialLinearGroup n R) : SpecialLinearGroup n R :=
  ⟨A.1.transpose, A.1.det_transpose ▸ A.2⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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