From de2d4b05ab40835cae5d6b67cbc35f90f483c0c4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 23 Jan 2024 20:10:09 +0900 Subject: [PATCH] changelog derive.v --- CHANGELOG_UNRELEASED.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4e6bd0d72c..4667967648 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -28,6 +28,9 @@ + instance using `isSemiAdditive.Build` for `\bar^d` + canonical `dEFin_snum` +- in `derive.v`: + + lemma `cvg_at_rightE`, `cvg_at_leftE` + ### Changed - in `boolp.v`: @@ -145,6 +148,13 @@ + canonicals `mule_monoid`, `mule_comoid` -> instance using `isComLaw.Build` + canonicals `maxe_monoid`, `maxe_comoid` -> instance using `isLaw.Build` +- in `derive.v` + + in notation `'d`, `differentiable`, `is_diff`: `[filter of ...]` -> `nbhs F` + + canonical `mulr_linear` -> instance using `isLinear.Build` + + canonical `mulr_rev_linear` -> instance using `isLinear.Build` + + canonical `mulr_bilinear` -> lemma `mulr_is_bilinear` and instance using `bilinear_isBilinear.Build` + + `set (set ...)` -> `set_system ...` + ### Renamed ### Generalized