Commit 2023-08-11 14:14 e8820b88

feat: continuous linear equivalences act transitively on nonzero vectors (#6346) 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.