mathlib3

c9d69a46 - feat(topology/algebra/module/finite_dimension): all linear maps from a finite dimensional T2 TVS are continuous (#13460)

feat(topology/algebra/module/finite_dimension): all linear maps from a finite dimensional T2 TVS are continuous (#13460) Summary of the changes : - generalize a bunch of results from `analysis/normed_space/finite_dimension` (main ones are : `continuous_equiv_fun_basis`, `linear_map.continuous_of_finite_dimensional`, and related constructions like `linear_map.to_continuous_linear_map`) to arbitrary TVSs, and move them to a new file `topology/algebra/module/finite_dimension` - generalize `linear_map.continuous_iff_is_closed_ker` to arbitrary TVSs, and move it from `analysis/normed_space/operator_norm` to the new file - as needed by the generalizations, add lemma `unique_topology_of_t2` : if `𝕜` is a nondiscrete normed field, any T2 topology on `𝕜` which makes it a topological vector space over itself (with the norm topology) is *equal* to the norm topology - finally, change `pi_eq_sum_univ` to take any `decidable_eq` instance (not just the classical ones), and fix later uses