Theorem Matrix.det_ne_zero_of_sum_col_pos

Modification history

2023-08-15 03:15
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean
feat: proof of Gershgorin's circle theorem and some applications (#6436) …
Added Matrix.det_ne_zero_of_sum_col_posView on Github →