row_transpose

Mathlib.LinearAlgebra.Matrix.Defs

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

English

The rows of the transpose of A equal the columns of A; i.e., A^T.row = A.col.

Русский

Строки транспонированной матрицы A равны столбцам A; то есть A^T.row = A.col.

LaTeX

$$$A^{\top}.row = A.col$$$

Lean4

@[simp]
theorem row_transpose (A : Matrix m n α) : Aᵀ.row = A.col :=
  rfl

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

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

Разделы

Аффилиация

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