English
There is a canonical linear isometry between G and the space of continuous multilinear maps 𝕜-valued on 𝑛 copies of 𝕜, i.e., the bijection G ≃ₗᵢ 𝔠ℑⁿ(𝕜, G) is given by z ↦ mkPiRing 𝕜 ι z with inverse f ↦ f(1,1,...,1).
Русский
Существует каноническое линейное изометрическое отображение между G и пространством непрерывных много-линейных отображений 𝕜-значащих на n копиях 𝕜, т.е. биекция G ≃ₗᵢ ContinuousMultilinearMap 𝕜 (ι → 𝕜) G, заданная z ↦ mkPiRing 𝕜 ι z с обратным отображением f ↦ f(1,1,...,1).
LaTeX
$$$ G \cong_{\text{lin-iso}} \mathrm{ContinuousMultilinearMap}_{\mathbb{k}} (\{ι\to \mathbb{k}\})\, G $$$
Lean4
theorem mkContinuousLinear_norm_le' (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') (C : ℝ)
(H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) : ‖mkContinuousLinear f C H‖ ≤ max C 0 :=
by
dsimp only [mkContinuousLinear]
exact LinearMap.mkContinuous_norm_le _ (le_max_right _ _) _
