det_zero_of_column_eq — Mathlib

English

If i ≠ j, then det(updateRow j (M i)) = 0.

Русский

Если i ≠ j, то det(обновлённая строка j равна M_i) = 0.

LaTeX

$$i \\\\neq j \\\\Rightarrow \\\\det(\\\\text{updateRow}(M, j, M_i)) = 0$$

Lean4

/-- If a matrix has a repeated column, the determinant will be zero. -/
theorem det_zero_of_column_eq (i_ne_j : i ≠ j) (hij : ∀ k, M k i = M k j) : M.det = 0 :=
  by
  rw [← det_transpose, det_zero_of_row_eq i_ne_j]
  exact funext hij

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