mathlib3

1e320130 - feat(analysis/normed_space/*exponential): more results about `star` (#18553)

feat(analysis/normed_space/*exponential): more results about `star` (#18553) These are trivial consequences of existing results. It turns out we already had a proof about `exp _ x` belonging to `unitary X`; this weakens the conditions.