mathlib3

0ce07501 - chore(linear_algebra/finite_dimensional): generalize from Type to Sort (#18723)

chore(linear_algebra/finite_dimensional): generalize from Type to Sort (#18723) The replacement of `fintype` with `finite` means there's no longer a need to handle these cases (added in #12877) separately. I verified that `{ι : Sort*}` is not being inferred as `{ι : Sort (u + 1)}`.