det_eq_zero_of_not_linearIndependent_cols

English

Let A be a square matrix over a domain R. If the columns of A are linearly dependent, then det(A) = 0.

Русский

Пусть A — квадратная матрица над областью R. Пусть столбцы A линейно зависимы. Тогда det(A) = 0.

LaTeX

$$$\\neg\\operatorname{LinearIndependent}_R\\bigl(\\lambda i, A^T i\\bigr) \\Rightarrow \\det A = 0$$$

Lean4

theorem det_eq_zero_of_not_linearIndependent_cols [IsDomain R] {A : Matrix m m R}
    (hA : ¬LinearIndependent R (fun i ↦ Aᵀ i)) : det A = 0 :=
  by
  contrapose! hA
  exact linearIndependent_cols_of_det_ne_zero hA

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