transpose_transpose

Mathlib.LinearAlgebra.Matrix.Defs

URI: https://scilib.ai/kg/mathlib#Matrix.transpose_transpose

English

Applying transpose twice returns the original matrix: (Mᵀ)ᵀ = M.

Русский

Два применения транспонирования возвращают исходную матрицу: (Mᵀ)ᵀ = M.

LaTeX

$$$ M^{\\mathrm{T}\\mathrm{T}} = M $$$

Lean4

@[simp]
theorem transpose_transpose (M : Matrix m n α) : Mᵀᵀ = M :=
  by
  ext
  rfl

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

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

Разделы

Аффилиация

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