From d844896e6418bb00418964bb4ae4219e2bd6b69c Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 25 Nov 2020 22:14:58 +0900 Subject: Rename `all1rel` to `all2rel`, restate `eq_allrel`, and add CHANGELOG entries Co-authored-by: Cyril Cohen --- mathcomp/field/separable.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/field/separable.v') diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index 7e208cd..d07839c 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -289,7 +289,7 @@ Variables (K : {vspace L}) (D : 'End(L)). (* the deriviations used here are going to be linear, so we only define *) (* the Derivation predicate for linear endomorphisms. *) Definition Derivation : bool := - all1rel (fun u v => D (u * v) == D u * v + u * D v) (vbasis K). + all2rel (fun u v => D (u * v) == D u * v + u * D v) (vbasis K). Hypothesis derD : Derivation. -- cgit v1.2.3