Theorem MeasureTheory.llr_smul_nnreal_same

Modification history

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