Theorem MeasureTheory.Memℒp.integrable_norm_rpow'

Modification history

2023-06-04 05:44

Mathlib/MeasureTheory/Function/L1Space.lean

style: recover `Is` of `Foo` which is ported from `is_foo` (#4639) …

Modified MeasureTheory.Memℒp.integrable_norm_rpow'View on Github →

2023-05-31 04:37

Mathlib/MeasureTheory/Function/L1Space.lean

feat: port MeasureTheory.Function.L1Space (#4383)

Added MeasureTheory.Memℒp.integrable_norm_rpow'View on Github →