mathlib3

bb2e7f9e - feat(algebra/star/pi): star operates elementwise on pi types (#7342)