mathlib
864a12e8 - chore(measure_theory/function/lp_space): use notation for `nnnorm` (#11039)

Commit

3 years ago

chore(measure_theory/function/lp_space): use notation for `nnnorm` (#11039)

Author

hrmacbeth

hrmacbeth

Parents

Loading