mathlib

bc9e38f4 - refactor(linear_algebra/dimension): remove some nontrivial assumptions (#9693)