mathlib3

ac76eb37 - feat(algebra/star/unitary): lemmas about group_with_zero (#11493)