Commit 2024-05-25 12:43 ea60bad3

View on Github →

feat: trace of a permutation matrix (#13086) To go with Matrix.det_permutation

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant.lean

deleted theorem Matrix.det_permutation

Created Mathlib/LinearAlgebra/Matrix/Permutation.lean

added theorem Matrix.det_permutation

added theorem Matrix.trace_permutation

Modified Mathlib/LinearAlgebra/Matrix/Trace.lean