Theorem Matrix.abs_det_submatrix_equiv_equiv

Modification history

2025-04-09 10:22
Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
chore: use mixin ordered algebraic typeclasses (part 2) (#20595)
Modified Matrix.abs_det_submatrix_equiv_equivView on Github →
2024-11-22 10:42
Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
feat: `Matrix.abs_det_submatrix_equiv_equiv` (#19332)
Added Matrix.abs_det_submatrix_equiv_equivView on Github →