English
If every row is strictly diagonally dominant by the sum of off-diagonal entries, then det(A) ≠ 0.
Русский
Если каждая строка строго доминирует по диагонали над суммой недиагональных элементов, то det(A) ≠ 0.
LaTeX
$$$\forall k, \sum_{j \neq k} \|A_{kj}\| < \|A_{kk}\| \Rightarrow \det A \neq 0$$$
Lean4
/-- If `A` is a row strictly dominant diagonal matrix, then it's determinant is nonzero. -/
theorem det_ne_zero_of_sum_row_lt_diag (h : ∀ k, ∑ j ∈ Finset.univ.erase k, ‖A k j‖ < ‖A k k‖) : A.det ≠ 0 :=
by
contrapose! h
suffices ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖) by
exact this.imp (fun a h ↦ by rwa [mem_closedBall_iff_norm', sub_zero] at h)
refine eigenvalue_mem_ball ?_
rw [Module.End.hasEigenvalue_iff, Module.End.eigenspace_zero, ne_comm]
exact ne_of_lt (LinearMap.bot_lt_ker_of_det_eq_zero (by rwa [LinearMap.det_toLin']))
