New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(Mathlib/LinearAlgebra/Basis): Move results about vector spaces to a new file #6321
Conversation
…to a new file This breaks a dependency cycle with `Module.Free`, which means we can immediately show that all vector spaces are free modules. The lemmas are moved without modification in this PR. A subsequent PR can use the `Module.Free` results to golf the vector space ones, and deduplicate the API.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks!
bors merge |
…to a new file (#6321) This breaks a dependency cycle with `Module.Free`, which means we can immediately show that all vector spaces are free modules. The lemmas are moved without modification in this PR. A subsequent PR can use the `Module.Free` results to golf the vector space ones, and deduplicate the API. Co-authored-by: Oliver Nash <github@olivernash.org>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
…to a new file (#6321) This breaks a dependency cycle with `Module.Free`, which means we can immediately show that all vector spaces are free modules. The lemmas are moved without modification in this PR. A subsequent PR can use the `Module.Free` results to golf the vector space ones, and deduplicate the API. Co-authored-by: Oliver Nash <github@olivernash.org>
…to a new file (#6321) This breaks a dependency cycle with `Module.Free`, which means we can immediately show that all vector spaces are free modules. The lemmas are moved without modification in this PR. A subsequent PR can use the `Module.Free` results to golf the vector space ones, and deduplicate the API. Co-authored-by: Oliver Nash <github@olivernash.org>
This breaks a dependency cycle with
Module.Free
, which means we can immediately show that all vector spaces are free modules.The lemmas are moved without modification in this PR. A subsequent PR can use the
Module.Free
results to golf the vector space ones, and deduplicate the API.