mathlib3

002b4528 - Show centroid_hom has a star operation