Commit 2025-08-11 22:14 2dcec534

refactor(Analysis/Normed/Module/Dual): Abbrev for strong dual (#27699) Replace NormedSpace.Dual with StrongDual.

• Add a new abbreviation StrongDual for M →L[R] R where the monoid M is a module over the semiring R and R and M are equipped with topologies;
• Remove the abbreviation NormedSpace.Dual and replace every reference to it with StrongDual;
• Move results which do not depend on a norm from Analysis/Normed/Module/Dual to a new file Topology/Algebra/Module/StrongDual and move them from the NormedSpace namespace to the StrongDual namespace;
• Move results which do not depend on a norm from the NormedSpace namespace in Analysis/Normed/Module/WeakDual to a new section at the start of that file in the StrongDual namespace;
• Add deprecated aliases for renamed results. Discussion: https://github.com/leanprover-community/mathlib4/pull/26345/files#r2234132483