Ruben Van de Velde

--- [](https://gitpod.io/from-referrer/)

This seems like a reasonable thing to split out, and it also makes `Associated.lean` not depend on as much order theory. --- [](https://gitpod.io/from-referrer/)

chore: drop order dependency from Data.Nat.Defs

3

--- - [ ] depends on: #13082 I tried to limit the scope as much as possible here; there's more in https://github.com/leanprover-community/mathlib4/compare/Nat-LinearOrder-2 and https://github.com/leanprover-community/mathlib4/compare/List.Basic-no-algebra [](https://gitpod.io/from-referrer/)

feat: trace of a permutation matrix

4

To go with Matrix.det_permutation --- Question: this adds several imports to state the theorem. Should it be put elsewhere? [](https://gitpod.io/from-referrer/)

--- Preliminary to removing the order dependency from `Mathlib/Data/Nat/Defs.lean`, but that needs a little more work [](https://gitpod.io/from-referrer/)

--- [](https://gitpod.io/from-referrer/)

chore: Move Nat.instLinearOrder to Init.Order.Defs

10

It turns out that pushing the dependency out is quite annoying, so as an alternative, we propose considering Preorder, PartialOrder and LinearOrder to be foundational type classes that all of...

feat: Int.prime_ofNat

2

--- [](https://gitpod.io/from-referrer/)

chore: deprecate Cardinal.mk'_def

3

--- [](https://gitpod.io/from-referrer/)

feat: some trivialities about Nat.primeCounting and Finset.filter

3

Also move some general results out of `PrimeCounting.lean`. --- [](https://gitpod.io/from-referrer/)