mathlib3
418f202b
- Update src/analysis/normed_space/lp_space.lean
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
Update src/analysis/normed_space/lp_space.lean Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
References
#15754 - feat(analysis/normed_space/lp_space): "functoriality" of `lp`
Author
eric-wieser
Parents
f28c79e5
Loading
