mathlib3

7f2b8064 - feat(analysis/inner_product_space/dual): complex Riesz representation theorem (#9924)

feat(analysis/inner_product_space/dual): complex Riesz representation theorem (#9924) Now that we have conjugate-linear maps, the Riesz representation theorem can be stated in a form that works over both `ℝ` and `ℂ`, as the construction of a conjugate-linear isometric equivalence from a complete inner product space `E` to its dual. Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca>