# Commit 2020-03-23 11:21 5b2c9521

View on Github →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