Commit 2021-09-29 04:03 d7abdff7
View on Github →chore(analysis/normed_space/*): prereqs for #8611 (#9379)
The functions abs and norm_sq on ℂ are proper.
A matrix with entries in a {seminormed group, normed group, normed space} is itself a {seminormed group, normed group, normed space}.
An injective linear map with finite-dimensional domain is a closed embedding.