Commit 2021-06-12 08:06 2016a93a

feat(linear_algebra): use finsets 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.