Commit 2025-09-18 17:28 1827e114

chore(Analysis/NormedSpace/Extend): split file (#29445) This PR accomplishes a few tasks:

1. splits the file according to whether the material needs the operator norm on continuous linear map. This will help us avoid importing the operator norm into LocallyConvex/ in an upcoming transition of material from NormedSpace/HahnBanach/ into other folders.
2. moves the resulting files out of the NormedSpace folder in accordance with #28698.
3. Cleans up the declarations / proofs / docstrings a small amount.
4. Uses Module.Dual spelling for the linear maps.

This is part of #28698 to migrate the material in Analysis/NormedSpace/ to other locations.