Generalize Riesz' theorem to locally compact T2 topological vector spaces

[ADedecker]

We have FiniteDimensional.of_locallyCompactSpace, which is the usual Riesz theorem for normed spaces.

More generally, Bourbaki proves the following: if K is a complete NontriviallyNormedField, then any T2 TVS over K which admits some totally bounded neighborhood of zero is finite dimensional.

[sharky564]

Hey, this is my first time trying to contribute to mathlib. I was able to compile a proof of this result by myself, although I subsequently used Gemini 3.0/3.1 to simplify and clean up most of it. Most of this simplification was the AI recognising Bornology made a lot of my proof redundant. I have not overwritten any of the existing theorems on the file, I have just added it separately, although I am not sure if there is a better location for it. I have got a PR of this here, and would appreciate any and all feedback.