Theorem MeasureTheory.Integrable.fun_smul

Modification history

2025-12-22 21:59
Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
refactor: use "@[to_fun]" to generate some lemmas (#32830)
Deleted MeasureTheory.Integrable.fun_smulView on Github →
2025-05-07 04:11
Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
feat(MeasureTheory): integral is monotone/convex if the integrand is monotone/convex (#24341) …
Added MeasureTheory.Integrable.fun_smulView on Github →