diff options
| author | Cyril Cohen | 2018-11-24 17:58:35 +0100 |
|---|---|---|
| committer | GitHub | 2018-11-24 17:58:35 +0100 |
| commit | add6e85884691faef1bf8742e803374815672cc2 (patch) | |
| tree | 2ffb41f5afa11a147989c8efcc1dcb295ae2ed2b /mathcomp/field/fieldext.v | |
| parent | 967088a6f87405a93ce21971392c58996df8c99f (diff) | |
| parent | f049e51c39077a025907ea87c08178dad1841801 (diff) | |
Merge pull request #249 from anton-trunov/prenex-implicits
Merge Arguments and Prenex Implicits
Diffstat (limited to 'mathcomp/field/fieldext.v')
| -rw-r--r-- | mathcomp/field/fieldext.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 2a905e9..881b888 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -696,7 +696,7 @@ move=> sKE; apply: minPoly_dvdp; last exact: root_minPoly. by apply: (polyOverSv sKE); rewrite minPolyOver. Qed. -Arguments Fadjoin_polyP [K x v]. +Arguments Fadjoin_polyP {K x v}. Lemma Fadjoin1_polyP x v : reflect (exists p, v = (map_poly (in_alg L) p).[x]) (v \in <<1; x>>%VS). Proof. @@ -737,13 +737,13 @@ Notation "'C_ ( E ) ( V )" := (capv_aspace E 'C(V)) Notation "E * F" := (prodv_aspace E F) : aspace_scope. Notation "f @: E" := (aimg_aspace f E) : aspace_scope. -Arguments Fadjoin_idP [F0 L K x]. -Arguments FadjoinP [F0 L K x E]. -Arguments Fadjoin_seqP [F0 L K rs E]. -Arguments polyOver_subvs [F0 L K p]. -Arguments Fadjoin_polyP [F0 L K x v]. -Arguments Fadjoin1_polyP [F0 L x v]. -Arguments minPoly_XsubC [F0 L K x]. +Arguments Fadjoin_idP {F0 L K x}. +Arguments FadjoinP {F0 L K x E}. +Arguments Fadjoin_seqP {F0 L K rs E}. +Arguments polyOver_subvs {F0 L K p}. +Arguments Fadjoin_polyP {F0 L K x v}. +Arguments Fadjoin1_polyP {F0 L x v}. +Arguments minPoly_XsubC {F0 L K x}. Section MapMinPoly. |