Theorem Matrix.det_zero

Modification history

2026-06-22 14:05

Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

chore(LinearAlgebra/Matrix): make `det_zero` simp (#40699) …

Modified Matrix.det_zero View on Github →

2023-04-20 10:27

Mathlib/LinearAlgebra/Matrix/Determinant.lean

feat: port LinearAlgebra.Matrix.Determinant (#3540)

Added Matrix.det_zero View on Github →