Commit 2024-11-22 10:42 dc8fc4ec

View on Github →

feat: Matrix.abs_det_submatrix_equiv_equiv (#19332)

Estimated changes

Modified Mathlib/Algebra/Order/Ring/Abs.lean

added theorem abs_unit_intCast

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

added theorem Matrix.abs_det_submatrix_equiv_equiv