det_eq_zero_of_not_linearIndependent_rows

English

If the rows of A are linearly dependent over IsDomain R, then det A = 0.

Русский

Если строки матрицы A линейно зависимы над полем IsDomain R, то det A = 0.

LaTeX

$$det A = 0 \\\\text{ if } \\\\text{LinearDependent}_R( A_i )$$

Lean4

theorem det_eq_zero_of_not_linearIndependent_rows [IsDomain R] {A : Matrix m m R}
    (hA : ¬LinearIndependent R (fun i ↦ A i)) : det A = 0 :=
  detRowAlternating.map_linearDependent A hA

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