diff options
| author | Kazuhiko Sakaguchi | 2020-11-25 22:14:58 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-11-25 22:29:55 +0900 |
| commit | d844896e6418bb00418964bb4ae4219e2bd6b69c (patch) | |
| tree | ccb40cfc9264241424aba156aa6e5289c9acfa8d /mathcomp/field | |
| parent | 43796130c3e59c0651a283e6654a7d82acbfeed3 (diff) | |
Rename `all1rel` to `all2rel`, restate `eq_allrel`, and add CHANGELOG entries
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/falgebra.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/separable.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index 97a5f22..8fb123e 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -1078,7 +1078,7 @@ Section Class_Def. Variables aT rT : FalgType K. Definition ahom_in (U : {vspace aT}) (f : 'Hom(aT, rT)) := - all1rel (fun x y : aT => f (x * y) == f x * f y) (vbasis U) && (f 1 == 1). + all2rel (fun x y : aT => f (x * y) == f x * f y) (vbasis U) && (f 1 == 1). Lemma ahom_inP {f : 'Hom(aT, rT)} {U : {vspace aT}} : reflect ({in U &, {morph f : x y / x * y >-> x * y}} * (f 1 = 1)) 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. |