-
Notifications
You must be signed in to change notification settings - Fork 297
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] - feat(linear_algebra/free_module): add class module.free #7801
Conversation
I decided to open a normal PR following the WIP PR #7722. There are of course other instances to add, and also start using this class somewhere :) |
Note that I changed the name of |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This PR looks great so far! Would you mind adding the universal property of the free module? I.e. that, for a free module |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…lib into class_free_mod
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.
LGTM
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.
nitpicks about names
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
We introduce here a new class `module.free`. Co-authored-by: Johan Commelin <johan@commelin.net>
Build failed (retrying...): |
We introduce here a new class `module.free`. Co-authored-by: Johan Commelin <johan@commelin.net>
Build failed (retrying...): |
We introduce here a new class `module.free`. Co-authored-by: Johan Commelin <johan@commelin.net>
Build failed (retrying...): |
We introduce here a new class `module.free`. Co-authored-by: Johan Commelin <johan@commelin.net>
Pull request successfully merged into master. Build succeeded: |
We introduce here a new class
module.free
.