Multilinear maps on finitely many finite-dimensional spaces are continuous

A multilinear map f : MultilinearMap 𝕜 M N on finitely many finite-dimensional Hausdorff topological vector spaces over a complete nontrivially normed field is continuous when addition and scalar multiplication are continuous in the codomain: MultilinearMap.continuous_of_finiteDimensional. The codomain need only be an additive commutative monoid. No norm is required on the domain modules or codomain, and no bound on the map is assumed.

This is the multilinear companion of LinearMap.continuous_of_finiteDimensional. Mathlib's MultilinearMap.continuous_of_bound asks for an explicit bound, which is exactly what one does not have when the multilinear map arrives from algebra — a tensor or symmetric-power construction, say — rather than from analysis.

theorem MultilinearMap.continuous_of_finiteDimensional {𝕜 : Type u_1} {ι : Type u_2} {M : ι → Type u_3} {N : Type u_4} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Finite ι] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module 𝕜 (M i)] [(i : ι) → TopologicalSpace (M i)] [∀ (i : ι), IsTopologicalAddGroup (M i)] [∀ (i : ι), ContinuousSMul 𝕜 (M i)] [∀ (i : ι), T2Space (M i)] [∀ (i : ι), FiniteDimensional 𝕜 (M i)] [AddCommMonoid N] [Module 𝕜 N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousSMul 𝕜 N] (f : MultilinearMap 𝕜 M N) : Continuous ⇑f

A multilinear map on finitely many finite-dimensional Hausdorff topological vector spaces over a complete nontrivially normed field is continuous when its codomain is an additive commutative monoid with continuous addition and scalar multiplication. No bound is required.