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



Co-authored-by: Christopher Hoskin <[email protected]>

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



Co-authored-by: Christopher Hoskin <[email protected]>

The `StrongDual` abbrev for `M →L[R] R`, where the monoid `M` is a module over the semiring `R` and `R` and `M` are equipped with topologies, was introduced in #27699.

This PR replaces existing occurrences of `M →L[R] R` with `StrongDual R M` etc. There are some exclusions:

- Bilinear forms `M →L[R] E →L[R] R` and where using  `StrongDual R M` would mask the symmetry of the statement;
- The dual of rings / fields `R →L[R] R` and similar;
- `WeakDual 𝕜 M` in `Topology/Algebra/Module/WeakDual`, where the focus is on the weak topology on `M →L[R] R`.

…over-community#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



Co-authored-by: Christopher Hoskin <[email protected]>

The `StrongDual` abbrev for `M →L[R] R`, where the monoid `M` is a module over the semiring `R` and `R` and `M` are equipped with topologies, was introduced in leanprover-community#27699.

This PR replaces existing occurrences of `M →L[R] R` with `StrongDual R M` etc. There are some exclusions:

- Bilinear forms `M →L[R] E →L[R] R` and where using  `StrongDual R M` would mask the symmetry of the statement;
- The dual of rings / fields `R →L[R] R` and similar;
- `WeakDual 𝕜 M` in `Topology/Algebra/Module/WeakDual`, where the focus is on the weak topology on `M →L[R] R`.

The `StrongDual` abbrev for `M →L[R] R`, where the monoid `M` is a module over the semiring `R` and `R` and `M` are equipped with topologies, was introduced in leanprover-community#27699.

This PR replaces existing occurrences of `M →L[R] R` with `StrongDual R M` etc. There are some exclusions:

- Bilinear forms `M →L[R] E →L[R] R` and where using  `StrongDual R M` would mask the symmetry of the statement;
- The dual of rings / fields `R →L[R] R` and similar;
- `WeakDual 𝕜 M` in `Topology/Algebra/Module/WeakDual`, where the focus is on the weak topology on `M →L[R] R`.

The `StrongDual` abbrev for `M →L[R] R`, where the monoid `M` is a module over the semiring `R` and `R` and `M` are equipped with topologies, was introduced in leanprover-community#27699.

This PR replaces existing occurrences of `M →L[R] R` with `StrongDual R M` etc. There are some exclusions:

- Bilinear forms `M →L[R] E →L[R] R` and where using  `StrongDual R M` would mask the symmetry of the statement;
- The dual of rings / fields `R →L[R] R` and similar;
- `WeakDual 𝕜 M` in `Topology/Algebra/Module/WeakDual`, where the focus is on the weak topology on `M →L[R] R`.

Also update the date to when the PR (#27699) was actually landed.

Also update the date to when the PR (leanprover-community#27699) was actually landed.

Also update the date to when the PR (leanprover-community#27699) was actually landed.