diff options
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/algC.v | 23 | ||||
| -rw-r--r-- | mathcomp/field/algnum.v | 8 | ||||
| -rw-r--r-- | mathcomp/field/closed_field.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/cyclotomic.v | 2 |
4 files changed, 18 insertions, 17 deletions
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index 4b37a9c..fc01763 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -607,7 +607,7 @@ Local Notation intrp := (map_poly intr). Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (@intr_inj _ : injective ZtoC). +Local Hint Resolve (@intr_inj _ : injective ZtoC) : core. (* Specialization of a few basic ssrnum order lemmas. *) @@ -645,7 +645,8 @@ Definition algC_algebraic x := Algebraics.Implementation.algebraic x. Lemma Creal0 : 0 \is Creal. Proof. exact: rpred0. Qed. Lemma Creal1 : 1 \is Creal. Proof. exact: rpred1. Qed. -Hint Resolve Creal0 Creal1. (* Trivial cannot resolve a general real0 hint. *) +(* Trivial cannot resolve a general real0 hint. *) +Hint Resolve Creal0 Creal1 : core. Lemma algCrect x : x = 'Re x + 'i * 'Im x. Proof. by rewrite [LHS]Crect. Qed. @@ -655,7 +656,7 @@ Proof. by rewrite Creal_Re. Qed. Lemma algCreal_Im x : 'Im x \is Creal. Proof. by rewrite Creal_Im. Qed. -Hint Resolve algCreal_Re algCreal_Im. +Hint Resolve algCreal_Re algCreal_Im : core. (* Integer subset. *) (* Not relying on the undocumented interval library, for now. *) @@ -680,7 +681,7 @@ Lemma floorCK : {in Cint, cancel floorC intr}. Proof. by move=> z /eqP. Qed. Lemma floorC0 : floorC 0 = 0. Proof. exact: (intCK 0). Qed. Lemma floorC1 : floorC 1 = 1. Proof. exact: (intCK 1). Qed. -Hint Resolve floorC0 floorC1. +Hint Resolve floorC0 floorC1 : core. Lemma floorCpK (p : {poly algC}) : p \is a polyOver Cint -> map_poly intr (map_poly floorC p) = p. @@ -723,7 +724,7 @@ Proof. by case/CintP=> m ->; apply: rpred_int. Qed. Lemma Cint0 : 0 \in Cint. Proof. exact: (Cint_int 0). Qed. Lemma Cint1 : 1 \in Cint. Proof. exact: (Cint_int 1). Qed. -Hint Resolve Cint0 Cint1. +Hint Resolve Cint0 Cint1 : core. Fact Cint_key : pred_key Cint. Proof. by []. Qed. Fact Cint_subring : subring_closed Cint. @@ -814,7 +815,7 @@ Proof. by case/CnatP=> n ->; apply: rpred_nat. Qed. Lemma Cnat_nat n : n%:R \in Cnat. Proof. by apply/CnatP; exists n. Qed. Lemma Cnat0 : 0 \in Cnat. Proof. exact: (Cnat_nat 0). Qed. Lemma Cnat1 : 1 \in Cnat. Proof. exact: (Cnat_nat 1). Qed. -Hint Resolve Cnat_nat Cnat0 Cnat1. +Hint Resolve Cnat_nat Cnat0 Cnat1 : core. Fact Cnat_key : pred_key Cnat. Proof. by []. Qed. Fact Cnat_semiring : semiring_closed Cnat. @@ -970,7 +971,7 @@ Proof. by move=> x_dv_y /dvdCP[m Zm ->]; apply: dvdC_mull. Qed. Lemma dvdC_refl x : (x %| x)%C. Proof. by apply/dvdCP; exists 1; rewrite ?mul1r. Qed. -Hint Resolve dvdC_refl. +Hint Resolve dvdC_refl : core. Fact dvdC_key x : pred_key (dvdC x). Proof. by []. Qed. Lemma dvdC_zmod x : zmod_closed (dvdC x). @@ -1004,7 +1005,7 @@ Lemma eqCmod_refl e x : (x == x %[mod e])%C. Proof. by rewrite /eqCmod subrr rpred0. Qed. Lemma eqCmodm0 e : (e == 0 %[mod e])%C. Proof. by rewrite /eqCmod subr0. Qed. -Hint Resolve eqCmod_refl eqCmodm0. +Hint Resolve eqCmod_refl eqCmodm0 : core. Lemma eqCmod0 e x : (x == 0 %[mod e])%C = (e %| x)%C. Proof. by rewrite /eqCmod subr0. Qed. @@ -1091,7 +1092,7 @@ Qed. Lemma Crat0 : 0 \in Crat. Proof. by apply/CratP; exists 0; rewrite rmorph0. Qed. Lemma Crat1 : 1 \in Crat. Proof. by apply/CratP; exists 1; rewrite rmorph1. Qed. -Hint Resolve Crat0 Crat1. +Hint Resolve Crat0 Crat1 : core. Fact Crat_key : pred_key Crat. Proof. by []. Qed. Fact Crat_divring_closed : divring_closed Crat. @@ -1236,5 +1237,5 @@ Proof. by move=> _ u /CintP[m ->]; apply: rpredZint. Qed. End PredCmod. End AlgebraicsTheory. -Hint Resolve Creal0 Creal1 Cnat_nat Cnat0 Cnat1 Cint0 Cint1 floorC0 Crat0 Crat1. -Hint Resolve dvdC0 dvdC_refl eqCmod_refl eqCmodm0. +Hint Resolve Creal0 Creal1 Cnat_nat Cnat0 Cnat1 Cint0 Cint1 floorC0 Crat0 Crat1 : core. +Hint Resolve dvdC0 dvdC_refl eqCmod_refl eqCmodm0 : core. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index 5d78cac..1db4aa4 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -56,7 +56,7 @@ Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (@intr_inj _ : injective ZtoC). +Local Hint Resolve (@intr_inj _ : injective ZtoC) : core. Local Notation QtoCm := [rmorphism of QtoC]. (* Number fields and rational spans. *) @@ -550,7 +550,7 @@ Proof. by rewrite Aint_Cint ?Cint_int. Qed. Lemma Aint0 : 0 \in Aint. Proof. exact: (Aint_int 0). Qed. Lemma Aint1 : 1 \in Aint. Proof. exact: (Aint_int 1). Qed. -Hint Resolve Aint0 Aint1. +Hint Resolve Aint0 Aint1 : core. Lemma Aint_unity_root n x : (n > 0)%N -> n.-unity_root x -> x \in Aint. Proof. @@ -702,7 +702,7 @@ Notation "x != y %[mod e ]" := (~~ (eqAmod e x y)) : algC_scope. Lemma eqAmod_refl e x : (x == x %[mod e])%A. Proof. by rewrite /eqAmod subrr rpred0. Qed. -Hint Resolve eqAmod_refl. +Hint Resolve eqAmod_refl : core. Lemma eqAmod_sym e x y : ((x == y %[mod e]) = (y == x %[mod e]))%A. Proof. by rewrite /eqAmod -opprB rpredN. Qed. @@ -739,7 +739,7 @@ Qed. Lemma eqAmodm0 e : (e == 0 %[mod e])%A. Proof. by rewrite /eqAmod subr0 unfold_in; case: ifPn => // /divff->. Qed. -Hint Resolve eqAmodm0. +Hint Resolve eqAmodm0 : core. Lemma eqAmodMr e : {in Aint, forall z x y, x == y %[mod e] -> x * z == y * z %[mod e]}%A. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index 009c1ae..76039d1 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -95,7 +95,7 @@ Definition qf_cps T D (x : cps T) := Lemma qf_cps_ret T D (x : T) : D x -> qf_cps D (ret x). Proof. move=> ??; exact. Qed. -Hint Resolve qf_cps_ret. +Hint Resolve qf_cps_ret : core. Lemma qf_cps_bind T1 D1 T2 D2 (x : cps T1) (f : T1 -> cps T2) : qf_cps D1 x -> (forall x, D1 x -> qf_cps D2 (f x)) -> qf_cps D2 (bind x f). diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index 80bdf50..afb0b0b 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -122,7 +122,7 @@ Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (@intr_inj [numDomainType of algC]). +Local Hint Resolve (@intr_inj [numDomainType of algC]) : core. Local Notation QtoC_M := (ratr_rmorphism [numFieldType of algC]). Lemma C_prim_root_exists n : (n > 0)%N -> {z : algC | n.-primitive_root z}. |