Theorem InformationTheory.IsUniquelyDecodable.flatten_injective

Modification history

2026-08-24 11:13

Mathlib/InformationTheory/Coding/UniquelyDecodable.lean

feat(InformationTheory/Coding): add Kraft inequality for prefix-free codes (#42584) …

Added InformationTheory.IsUniquelyDecodable.flatten_injective View on Github →