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] - split(analysis/convex/combination): split off analysis.convex.basic
#9115
Conversation
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.
This also adds set.finite.convex_hull_eq_image
and mem_Icc_of_mem_std_simplex
, right?
Can you update the module doc of convex/basic
?
Oh whoops, my change to the module docstring got lost in branch translation. Yes, those two lemmas use |
The module doc of |
bors merge |
Pull request successfully merged into master. Build succeeded: |
analysis.convex.basic
analysis.convex.basic
This moves
finset.center_mass
into its own new file.About the copyright header,
finset.center_mass
comes from #1804, which was written by Yury in December 2019.This can through right now with the convexity refactor.