mathlib

2016a93a - feat(linear_algebra): use `finset`s to define `det` and `trace` (#7778)

feat(linear_algebra): use `finset`s to define `det` and `trace` (#7778) This PR replaces `∃ (s : set M) (b : basis s R M), s.finite` with `∃ (s : finset M), nonempty (basis s R M)` in the definitions in `linear_map.det` and `linear_map.trace`. This should make it much easier to unfold those definitions without having to modify the instance cache or supply implicit params. In particular, it should help a lot with #7667.