From 16f89d45fee7c0e7b168dc0697d3dce0f29be150 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 3 Dec 2024 22:41:50 +0900 Subject: [PATCH] fix changelog --- CHANGELOG_UNRELEASED.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 83f356738..08c7e13dd 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -12,6 +12,7 @@ - in `mathcomp_extra.v`: + lemma `partition_disjoint_bigfcup` + - in `constructive_ereal.v`: + notations `\prod` in scope ereal_scope + lemmas `prode_ge0`, `prode_fin_num`