Theorem InformationTheory.klDiv_ne_top

Modification history

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