Commit 2022-06-03 10:31 c9d69a46

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