mathlib3

fbf3c643 - chore(analysis/normed_space/star): golf some lemmas (#11600)