Theorem MeasureTheory.Measure.rnDeriv_smul_same

Modification history

2026-03-03 19:57
Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean
feat: `klDiv` and scalar multiplication (#35301) …
Added MeasureTheory.Measure.rnDeriv_smul_sameView on Github →