Commit 2021-10-25 17:42 f298c559
View on Github →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.
- depends on: #9860