Commit 2021-09-30 18:34 4091f72b
View on Github →refactor(linear_algebra/free_module): split in two files (#9407)
We split linear_algebra/free_module in linear_algebra/free_module/basic and linear_algebra/free_module/finite, so one can work with free modules without having to import all the theory of dimension.