Note a renaming suggestion

weng-chenghui · web-flow · commit f0e8568d23f9 · 2026-02-27T14:54:19.000+09:00
diff --git a/dumas2017dual/lib/extra_entropy.v b/dumas2017dual/lib/extra_entropy.v
@@ -234,6 +234,7 @@ Qed.
 
 (* Unique point mass characterization: H(Z) = 0 iff there exists UNIQUE z
    with Pr[Z = z] = 1. Strengthens zero_entropy_eq_point_mass1 with uniqueness. *)
+  (* TODO: Should be renamed to entropy_eq0P *)
 Lemma zero_entropy_eq_point_mass
   (V: finType)
   (Z : {RV P -> V}) :
