mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(analysis/normed_space/lp_space): "functoriality" of `lp`

Open ADedecker opened this issue 3 years ago • 1 comments

Open in Gitpod

ADedecker avatar Jul 29 '22 16:07 ADedecker

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

mcdoll avatar Oct 02 '22 12:10 mcdoll

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

I think this comment still applies

eric-wieser avatar Mar 18 '23 13:03 eric-wieser