Commit 2023-03-12 22:38 1e320130
View on Github →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.