Theorem MeasureTheory.llr_smul_inv_left_eq_smul_right

Modification history

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