Theorem InformationTheory.toReal_klDiv_smul_left

Modification history

2026-03-03 19:57
Mathlib/InformationTheory/KullbackLeibler/Basic.lean
feat: `klDiv` and scalar multiplication (#35301) …
Added InformationTheory.toReal_klDiv_smul_leftView on Github →