changelog

math-comp · Dec 20, 2024 · 15ff83a · 15ff83a
1 parent 25c3e67
commit 15ff83a
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -35,10 +35,16 @@
 - in `probability.v`
   + lemma `integral_distribution` (existsing lemma `integral_distribution` has been renamed)
 
+- in `numfun.v`
+	+ lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp`
+
 ### Changed
 
 - in `lebesgue_integrale.v`
   + change implicits of `measurable_funP`
+
+- in `numfun.v`
+	+ lock `funepos`, `funeneg`
 
 ### Renamed