mathlib
b9ad7333
- split(analysis/convex/combination): split off `analysis.convex.basic` (#9115)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
split(analysis/convex/combination): split off `analysis.convex.basic` (#9115) 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.
Author
YaelDillies
Parents
62de5912
Loading