Commit 2025-09-25 08:21 eb2aba5a
View on Github →refactor(LinearAlgebra/Matrix): move lemmas around to reduce imports (#29709)
This makes results such as Matrix.det_one_sub_mul_comm and Matrix.eval_det more accessible.
From https://github.com/leanprover-community/mathlib4/pull/29709#issuecomment-3297172309,
| File | Base Count | Head Count | Change | |