Theorems · Theorem · linear algebra

Matrix.det_ne_zero_of_sum_col_pos

∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
  [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
  (Pairwise fun i j => A i j < 0) → (∀ (j : n), 0 < ∑ i, A i j) → A.det ≠ 0

A matrix whose nondiagonal entries are negative with the sum of the entries of each column positive has nonzero determinant.

Defined in

Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Cited by

1 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqCommRingLinearOrderIsStrictOrderedRing