mathlib

1cd74b11 - fix(linear_algebra/finite_dimensional): universe generalize cardinal_mk_le_findim_of_linear_independent (#3721)