diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index b8287296e4..b4d5226ada 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -68,6 +68,9 @@
 - in `measure.v`:
   + lemma `measurableID`
 
+- in `mathcomp_extra.v`:
+  + lemma `invf_ltp`
+
 ### Changed
 
 - in `forms.v`: