Theorem MeasureTheory.Measure.AbsolutelyContinuous.smul_right

Modification history

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