Commit 2021-09-15 18:42 244285c9
View on Github →feat(linear_algebra/free_module): add instances (#9087)
We add some module.finite instances. These are in the linear_algebra/free_module.lean files since they concern free modules.
From LTE
feat(linear_algebra/free_module): add instances (#9087)
We add some module.finite instances. These are in the linear_algebra/free_module.lean files since they concern free modules.
From LTE