updated changelog

math-comp · Oct 29, 2024 · 6835511 · 6835511
1 parent d6d5deb
commit 6835511
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -57,6 +57,11 @@
     `locally_compact_completely_regular`, and
     `completely_regular_regular`.
 
+- in file `realfun.v`,
+  + new lemmas `cauchy_MVT`,
+    `lhopital_right`, and
+    `lhopital_left`.
+
 ### Changed
 
 - in file `normedtype.v`,