mathlib

5b2c9521 - feat(analysis/convex.cone): prove M. Riesz extension theorem, Hahn-Banach theorem (#2120)

feat(analysis/convex.cone): prove M. Riesz extension theorem, Hahn-Banach theorem (#2120) * feat(analysis/convex.cone): prove M. Riesz extension theorem WIP * Complete the proof TODO: move many facts to `linear_algebra/basic`, fix possible build failures in other files * Fix compile of `analysis/convex/cone` * Cleanup, rewrite using `linear_pmap`s * Deduce Hahn-Banach theorem from M. Riesz extension theorem * Fix lint * Apply suggestions from code review [skip_ci] Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Expand comments, prove properties of `convex.to_cone`. * Docstrings * Apply suggestions from code review Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Update src/analysis/convex/cone.lean * Update src/linear_algebra/basic.lean Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>