mathlib

f298c559 - refactor(linear_algebra/finite_dimensional): define finite_dimensional using module.finite (#9854)

refactor(linear_algebra/finite_dimensional): define finite_dimensional using module.finite (#9854) `finite_dimensional K V` is by definition `is_noetherian K V`. We refactor this to use everywhere `finite K V` instead. To keep the PR reasonably small, we don't delete `finite_dimension`, but we define it as `module.finite`. In a future PR we will remove it. - [x] depends on: #9860