@[reducible, inline]

abbrev DualSpace.Dual (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (V : Type u_2) [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] : Type (max u_2 u_1)

The dual space V' = 𝓑(V, 𝕜) of a normed vector space V over a field 𝕜, defined as the space of bounded (continuous) linear functionals V →L[𝕜] 𝕜. An element of Dual 𝕜 V is called a functional. When 𝕜 = ℝ or ℂ, the completeness of 𝕜 makes Dual 𝕜 V a Banach space.