fix changelog

math-comp · Nov 10, 2024 · 8dcefbc · 8dcefbc
1 parent 49d896b
commit 8dcefbc
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -71,8 +71,6 @@
   + lemma `countable_measurable`
 - in `realfun.v`:
   + lemma `cvgr_dnbhsP`
-  + new definitions `left_assoc_prod`, and `right_assoc_prod`.
-  + new lemmas `left_assoc_prodK`, `right_assoc_prodK`, and `swapK`.
   + new definitions `prodA`, and `prodAr`.
   + new lemmas `prodAK`, `prodArK`, and `swapK`.
 - in file `product_topology.v`,