-
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/affine_space): affine combinations for finsets #3122
Conversation
Extend the definitions of affine combinations over a `fintype` to the case of sums over a `finset` of an arbitrary index type (which is appropriate for use cases such as affine independence of a possibly infinite family of points), with the original definitions and results for a `fintype` (which is appropriate for more concrete use cases such as barycentric coordinates in a triangle, where the type is `fin 3`) then being defined using those definitions and `finset.univ`.
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
Canceled. |
Hmm, seems there are still some small problems. But overall, I'm happy with how this looks. bors d+ |
✌️ jsm28 can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…3122) Extend the definitions of affine combinations over a `fintype` to the case of sums over a `finset` of an arbitrary index type (which is appropriate for use cases such as affine independence of a possibly infinite family of points). Also change to have only bundled versions of `weighted_vsub_of_point` and `weighted_vsub`, following review, so avoiding duplicating parts of `linear_map` API.
Pull request successfully merged into master. Build succeeded: |
…eanprover-community#3122) Extend the definitions of affine combinations over a `fintype` to the case of sums over a `finset` of an arbitrary index type (which is appropriate for use cases such as affine independence of a possibly infinite family of points). Also change to have only bundled versions of `weighted_vsub_of_point` and `weighted_vsub`, following review, so avoiding duplicating parts of `linear_map` API.
Extend the definitions of affine combinations over a
fintype
to thecase of sums over a
finset
of an arbitrary index type (which isappropriate for use cases such as affine independence of a possibly
infinite family of points).
Also change to have only bundled versions of
weighted_vsub_of_point
and
weighted_vsub
, following review, so avoiding duplicating partsof
linear_map
API.