emptyCols_isTotallyUnimodular — Mathlib

English

If the index type for columns is empty, any matrix is totally unimodular (via transpose of empty rows).

Русский

Если множество индексов столбцов пусто, любая матрица тотально унимодулярна (через транспонирование пустых строк).

LaTeX

$$IsEmpty(n) \\Rightarrow A.IsTotallyUnimodular$$

Lean4

/-- If `A` has no columns, then it is totally unimodular. -/
@[simp]
theorem emptyCols_isTotallyUnimodular [IsEmpty n] (A : Matrix m n R) : A.IsTotallyUnimodular :=
  A.transpose.emptyRows_isTotallyUnimodular.transpose

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