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/barycentric_coords): define barycentric coordinates #9472
Conversation
ocfnash
commented
Sep 30, 2021
/-- The sum of the coordinates of an element `m : M` with respect to a basis. -/ | ||
noncomputable def sum_coords : M →ₗ[R] R := | ||
finsupp.lsum ℕ (λ i, linear_map.id) ∘ₗ (b.repr : M →ₗ[R] ι →₀ R) |
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.
Do you have a use-case in mind outside of barycentric coordinates? I'd be inclined to put this in that file if not.
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.
On reflection I think you're right but maybe I'll canvass an opinion from @Vierkantor before I move things.
(Edit: to answer your question, I do not have another use-case in mind though I expect there will be others eventually.)
Thanks 🎉 bors merge |
Pull request successfully merged into master. Build succeeded: |