English
A matrix with negative off-diagonal entries and positive column sums has nonzero determinant.
Русский
Матрица с отрицательными элементами вне диагонали и положительными суммами столбцов имеет ненулевой детерминант.
LaTeX
$$$\\det A \\neq 0$ under column-sum positivity and negative off-diagonal$$
Lean4
/-- A matrix whose nondiagonal entries are negative with the sum of the entries of each
row positive has nonzero determinant. -/
theorem det_ne_zero_of_sum_row_pos [DecidableEq n] {S : Type*} [CommRing S] [LinearOrder S] [IsStrictOrderedRing S]
{A : Matrix n n S} (h1 : Pairwise fun i j => A i j < 0) (h2 : ∀ i, 0 < ∑ j, A i j) : A.det ≠ 0 :=
by
rw [← Matrix.det_transpose]
refine det_ne_zero_of_sum_col_pos ?_ ?_
· simp_rw [Matrix.transpose_apply]
exact fun i j h => h1 h.symm
· simp_rw [Matrix.transpose_apply]
exact h2
