mathlib

4843bb12 - chore(linear_algebra/finsupp_vector_space): remove leftover pp.universes (#3081)