[Merged by Bors] - feat: continuous linear equivalences act transitively on nonzero vectors

[sgouezel]

For any nonzero vectors, one can find a continuous linear equivalence sending the first one to the second one. This follows from the existence of nontrivial linear forms, whichis proved in mathlib in the two following situations:

• normed spaces over R or C
• locally convex vector spaces over R
  To obtain a statement that applies in these two cases, we introduce a new typeclass SeparatingDual.

---

[ADedecker]

Is the plan to remove this new typeclass once we have a satisfying statement for the Hahn-Banach theorem? Or do you want to keep it anyways (e.g because it would apply to finite dimensional spaces over any field)?

[sgouezel]

I don't think we can hope to have a single version of Hahn-Banach that covers all interesting examples (e.g. spherically complete nonarchimedean fields), so I expect this class will stay.

[ADedecker]

Thanks!

bors d+

[bors]

✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[sgouezel]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style