det_ne_zero_of_sum_col_lt_diag — Mathlib

English

If every column is strictly diagonally dominant by the sum of off-diagonal entries, then det(A) ≠ 0.

Русский

Если каждый столбец строго доминирует по диагонали над суммой недиагональных элементов, det(A) ≠ 0.

LaTeX

$$$\forall k, \sum_{i \neq k} \|A_{ik}\| < \|A_{kk}\| \Rightarrow \det A \neq 0$$$

Lean4

/-- If `A` is a column strictly dominant diagonal matrix, then it's determinant is nonzero. -/
theorem det_ne_zero_of_sum_col_lt_diag (h : ∀ k, ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖) : A.det ≠ 0 :=
  by
  rw [← Matrix.det_transpose]
  exact det_ne_zero_of_sum_row_lt_diag (by simp_rw [Matrix.transpose_apply]; exact h)

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