mathlib

137163a8 - feat(analysis/normed_space/dual): Fréchet-Riesz representation for the dual of a Hilbert space (#4379)

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`. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>