Theorem MeasureTheory.setIntegral_rnDeriv_smul

Modification history

2024-11-05 08:41

Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

refactor(HasPDF): use structure fields (#18371) …

Modified MeasureTheory.setIntegral_rnDeriv_smul View on Github →

2024-08-29 16:54

Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

feat (MeasureTheory.Integral): Generalize lemmas to `setIntegral` and `setLIntegral` (#15551) …

Added MeasureTheory.setIntegral_rnDeriv_smul View on Github →