Commit 2020-11-28 16:26 137163a8

feat(analysis/normed_space/dual): Fréchet-Riesz representation for the dual of a Hilbert space (#4379) This PR defines to_dual which maps an element x of an inner product space to λ y, ⟪x, y⟫. We also give the Fréchet-Riesz representation, which states that every element of the dual of a Hilbert space E has the form λ u, ⟪x, u⟫ for some x : E.