basic): golf a proof (#12420)

Commit

3 years ago

chore(analysis/normed_space/star/basic): golf a proof (#12420) Shorten a proof using ext.

Author

adomani

Parents