transpose_empty_rows

Mathlib.LinearAlgebra.Matrix.Notation

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

English

The transpose of a matrix with a zero number of columns is the matrix of empty rows.

Русский

Транспонирование матрицы с нулём столбцов даёт матрицу пустых строк.

LaTeX

$$$A^T = \\mathrm{of}(![])$ for $A: M' (\\mathrm{Fin}\\,0)\\; α$$$

Lean4

@[simp]
theorem transpose_empty_rows (A : Matrix m' (Fin 0) α) : Aᵀ = of ![] :=
  empty_eq _

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

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

Разделы

Аффилиация

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