mathlib3

9851a0a9 - Merge branch 'non-assoc-star-mul' into centroid_star