Moritz Doll

I don't really feel comfortable reviewing this, the code looks good, but I cannot judge whether this makes sense mathematically.

The assertion is true modulo distinguishing between `continuous_linear_map` and `linear_map` and when your `linear_map`s are not a special kind of `linear_pmap`s (which is an implementation detail). The point why mathematicians...

It is well-known that you can prove this by showing stuff about continuous seminorms (this is for instance done in Narici-Beckenstein). My reason for not doing that way was that...

I am not sure whether we want to have a definition for absolutely convex sets. It is only two properties, but on the other side barrels need additionally need absorbing...

when this was discussed someone mentioned that Bhavik has a proof, but if he does not PR it into mathlib I see no problem having it as a possible first...

bors merge

I guess we want to keep some of theorems in `hahn_banach/extension` with the norm as corollaries. I have no strong opinion on when to move the things, if you do...

Thanks. maintainer merge

Please add an empty line before the dashed line. Also you have to merge master and fix the merge conflicts (you can do that in github).

Could you add section titles for `linear_isometry` and `congr_right` and some documentation in the module docstring of `lp_spaces`?