From 783631c771ec76baa4ff9d292c1eddfb58f67f4c Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 20 Nov 2020 16:52:52 +0900 Subject: Generalize `allrel` to take two lists as arguments --- mathcomp/field/falgebra.v | 11 +++++------ mathcomp/field/separable.v | 13 ++++++------- 2 files changed, 11 insertions(+), 13 deletions(-) (limited to 'mathcomp/field') diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index 9069818..97a5f22 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -1078,21 +1078,20 @@ Section Class_Def. Variables aT rT : FalgType K. Definition ahom_in (U : {vspace aT}) (f : 'Hom(aT, rT)) := - let fM_at x y := f (x * y) == f x * f y in - all (fun x => all (fM_at x) (vbasis U)) (vbasis U) && (f 1 == 1). + all1rel (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)) (ahom_in U f). Proof. -apply: (iffP andP) => [[/allP fM /eqP f1] | [fM f1]]; last first. - rewrite f1; split=> //; apply/allP=> x Ax; apply/allP=> y Ay. +apply: (iffP andP) => [[/allrelP fM /eqP f1] | [fM f1]]; last first. + rewrite f1; split=> //; apply/allrelP => x y Ax Ay. by rewrite fM // vbasis_mem. -split=> // x y /coord_vbasis -> /coord_vbasis ->. +split=> // x y /coord_vbasis -> /coord_vbasis ->. rewrite !mulr_suml ![f _]linear_sum mulr_suml; apply: eq_bigr => i _ /=. rewrite !mulr_sumr linear_sum; apply: eq_bigr => j _ /=. rewrite !linearZ -!scalerAr -!scalerAl 2!linearZ /=; congr (_ *: (_ *: _)). -by apply/eqP/(allP (fM _ _)); apply: memt_nth. +by apply/eqP/fM; apply: memt_nth. Qed. Lemma ahomP {f : 'Hom(aT, rT)} : reflect (lrmorphism f) (ahom_in {:aT} f). diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index 6320343..7e208cd 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -288,8 +288,8 @@ Variables (K : {vspace L}) (D : 'End(L)). (* A deriviation only needs to be additive and satify Lebniz's law, but all *) (* the deriviations used here are going to be linear, so we only define *) (* the Derivation predicate for linear endomorphisms. *) -Definition Derivation (s := vbasis K) : bool := - all (fun u => all (fun v => D (u * v) == D u * v + u * D v) s) s. +Definition Derivation : bool := + all1rel (fun u v => D (u * v) == D u * v + u * D v) (vbasis K). Hypothesis derD : Derivation. @@ -299,7 +299,7 @@ move=> u v /coord_vbasis-> /coord_vbasis->. rewrite !(mulr_sumr, linear_sum) -big_split; apply: eq_bigr => /= j _. rewrite !mulr_suml linear_sum -big_split; apply: eq_bigr => /= i _. rewrite !(=^~ scalerAl, linearZZ) -!scalerAr linearZZ -!scalerDr !scalerA /=. -by congr (_ *: _); apply/eqP; rewrite (allP (allP derD _ _)) ?memt_nth. +by congr (_ *: _); apply/eqP/(allrelP derD); exact: memt_nth. Qed. Lemma Derivation_mul_poly (Dp := map_poly D) : @@ -314,7 +314,7 @@ End Derivation. Lemma DerivationS E K D : (K <= E)%VS -> Derivation E D -> Derivation K D. Proof. -move/subvP=> sKE derD; apply/allP=> x Kx; apply/allP=> y Ky; apply/eqP. +move/subvP=> sKE derD; apply/allrelP=> x y Kx Ky; apply/eqP. by rewrite (Derivation_mul derD) ?sKE // vbasis_mem. Qed. @@ -492,8 +492,7 @@ Qed. Lemma extendDerivationP : separable_element K x -> Derivation <> (extendDerivation K). Proof. -move=> sep; apply/allP=> u /vbasis_mem Hu; apply/allP=> v /vbasis_mem Hv. -apply/eqP. +move=> sep; apply/allrelP=> u v /vbasis_mem Hu /vbasis_mem Hv; apply/eqP. rewrite -(Fadjoin_poly_eq Hu) -(Fadjoin_poly_eq Hv) -hornerM. rewrite !{1}extendDerivation_horner ?{1}rpredM ?Fadjoin_polyOver //. rewrite (Derivation_mul_poly derD) ?Fadjoin_polyOver //. @@ -528,7 +527,7 @@ have DK_0: (K <= lker D)%VS. apply/subvP=> v Kv; rewrite memv_ker lfunE /= Fadjoin_polyC //. by rewrite derivC horner0. have Dder: Derivation <> D. - apply/allP=> u /vbasis_mem Kx_u; apply/allP=> v /vbasis_mem Kx_v; apply/eqP. + apply/allrelP=> u v /vbasis_mem Kx_u /vbasis_mem Kx_v; apply/eqP. rewrite !lfunE /=; set Px := Fadjoin_poly K x. set Px_u := Px u; rewrite -(Fadjoin_poly_eq Kx_u) -/Px -/Px_u. set Px_v := Px v; rewrite -(Fadjoin_poly_eq Kx_v) -/Px -/Px_v. -- cgit v1.2.3 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/falgebra.v | 2 +- mathcomp/field/separable.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp/field') 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. -- cgit v1.2.3