rank): remove `module.free` assumption (#18792)

Commit

2 years ago

feat(linear_algebra/free_module/finite/rank): remove `module.free` assumption (#18792) Combined with the result in #18787, this lets us golf a downstream proof about matrices.

Author

eric-wieser

Parents

814d76e2

mathlib b5b5dd5a - feat(linear_algebra/free_module/finite/rank): remove `module.free` assumption (#18792)

mathlib
b5b5dd5a - feat(linear_algebra/free_module/finite/rank): remove `module.free` assumption (#18792)