mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard
verified publisher icon leanprover-community

feat: trace of a permutation matrix

Open Ruben-VandeVelde opened this issue 1 year ago • 4 comments

To go with Matrix.det_permutation

Question: this adds several imports to state the theorem. Should it be put elsewhere?

Open in Gitpod

Ruben-VandeVelde avatar May 21 '24 15:05 Ruben-VandeVelde

Question: this adds several imports to state the theorem. Should it be put elsewhere?

The safe answer would be yes!

dupuisf avatar May 22 '24 10:05 dupuisf

Okay, suggestions? :)

Ruben-VandeVelde avatar May 22 '24 11:05 Ruben-VandeVelde

Does #find_home say anything interesting?

dupuisf avatar May 22 '24 14:05 dupuisf

Nothing at all

Ruben-VandeVelde avatar May 22 '24 20:05 Ruben-VandeVelde

New file then?

dupuisf avatar May 23 '24 11:05 dupuisf

Looks good!

bors r+

dupuisf avatar May 25 '24 12:05 dupuisf

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar May 25 '24 13:05 mathlib-bors[bot]