Square_Matrix_with_Duplicate_Rows_has_Zero_Determinant
Proveddeterminantlinear-algebramatrixproofwiki
If two rows of a square matrix over a commutative ring are the same, then its determinant is zero.
Preamble
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Formal statement
theorem Square_Matrix_with_Duplicate_Rows_has_Zero_Determinant {R : Type _} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (i j : Fin n) (hij : i ≠ j) (hdup : A i = A j) : A.det = 0 := by sorrySource