Commit 2021-09-08 08:23 8341d165

feat(linear_algebra/finite_dimensional): make finite_dimensional_bot an instance (#9053) This was previously made into a local instance in several places, but there appears to be no reason it can't be a global instance. cf discussion at #8884.