emptyRows_isTotallyUnimodular — Mathlib

English

If the index type for rows is empty, any matrix is totally unimodular.

Русский

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

LaTeX

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

Lean4

/-- If `A` has no rows, then it is totally unimodular. -/
@[simp]
theorem emptyRows_isTotallyUnimodular [IsEmpty m] (A : Matrix m n R) : A.IsTotallyUnimodular :=
  by
  intro k f _ _ _
  cases k with
  | zero => use 1; rw [submatrix_empty, det_fin_zero, SignType.coe_one]
  | succ => exact (IsEmpty.false (f 0)).elim

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