Theorem Finset.card_filter_length_eq_le

Modification history

2026-02-17 15:39
Mathlib/Data/Fintype/BigOperators.lean
feat(InformationTheory/Coding): Kraft-McMillan inequality for uniquely decodable codes (#34108) …
Added Finset.card_filter_length_eq_leView on Github →