Commit 2025-11-06 19:26 04e6d449

chore(Analysis/NormedSpace/HahnBanach): move and split files (#29447) This moves or splits the files in Analysis/NormedSpace/HahnBanach/ accordingly:

• Separation → Analysis/LocallyConvex/Separation
• Extension → Analysis/Normed/Module/HahnBanach
• SeparatingDual: split, mostly in Analysis/LocallyConvex/SeparatingDual, but a few completeness results are sent to Analysis/Normed/Operator/CompleteCodomain. The split allows us to significantly reduce the imports of SeparatingDual, albeit with a new proof that a normed space over RCLike 𝕜 has a separating dual. Here we use the geometric Hahn-Banach theorem instead of the analytic one. This is part of #28698 to migrate the material in Analysis/NormedSpace/ to other locations.