Theorem InformationTheory.IsPrefixFree.finsetSum_one_div_card_pow_length_le_one

Modification history

2026-08-24 11:13
Mathlib/InformationTheory/Coding/Kraft.lean
feat(InformationTheory/Coding): add Kraft inequality for prefix-free codes (#42584) …
Added InformationTheory.IsPrefixFree.finsetSum_one_div_card_pow_length_le_oneView on Github →