mathlib

8341d165 - feat(linear_algebra/finite_dimensional): make finite_dimensional_bot an instance (#9053)

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.