fix changelog

math-comp · Aug 22, 2023 · 0aa51a1 · 0aa51a1
1 parent eb04917
commit 0aa51a1
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -30,8 +30,8 @@
 - in `constructive_ereal.v`:
   + lemma `eqe_pdivr_mull`
 
-- in `lebesgue_integral.v`:
-  + definition `Lnorm`, notations `'N[mu]_p[f]`, `` `|| f ||_p ``
+- new file `hoelder.v`:
+  + definition `Lnorm`, notations `'N[mu]_p[f]`, `'N_p[f]`
   + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0`
   + lemma `hoelder`