transpose_empty_cols

Mathlib.LinearAlgebra.Matrix.Notation

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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