Commit 2026-06-22 14:05 bbd5fcf3
View on Github →chore(LinearAlgebra/Matrix): make det_zero simp (#40699)
This used to be provable by simp back when det was an abbrev. This changed in #33590.
This dates back all the way from https://github.com/leanprover-community/mathlib3/pull/404, and in fact the code came from the even earlier https://github.com/leanprover-community/mathlib3/pull/378. Neither of the PRs offers an explanation for why this argument was explicit.
From BrauerGroup and RealRooted